1  /-
  2  Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Robert Y. Lewis
  5  -/
  6  
  7  import data.padics.padic_integers data.polynomial topology.metric_space.cau_seq_filter
src         └────────────────────────┘ └─────────────┘ └──────────────────────────────────┘
  8  import analysis.specific_limits topology.algebra.polynomial
src         └──────────────────────┘ └─────────────────────────┘
  9  
 10  /-!
 11  # Hensel's lemma on ℤ_p
 12  
 13  This file proves Hensel's lemma on ℤ_p, roughly following Keith Conrad's writeup:
 14  <http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf>
 15  
 16  Hensel's lemma gives a simple condition for the existence of a root of a polynomial.
 17  
 18  The proof and motivation are described in the paper
 19  [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019].
 20  
 21  ## References
 22  
 23  * <http://www.math.uconn.edu/~kconrad/blurbs/gradnumthy/hensel.pdf>
 24  * [R. Y. Lewis, *A formal proof of Hensel's lemma over the p-adic integers*][lewis2019]
 25  * <https://en.wikipedia.org/wiki/Hensel%27s_lemma>
 26  
 27  ## Tags
 28  
 29  p-adic, p adic, padic, p-adic integer
 30  -/
 31  
 32  noncomputable theory
 33  
 34  open_locale classical topological_space
 35  
 36  -- We begin with some general lemmas that are used below in the computation.
 37  
 38  lemma padic_polynomial_dist {p : ℕ} [p.prime] (F : polynomial ℤ_[p]) (x y : ℤ_[p]) :
id                                       └────┘       └────────┘ └─┘         └─┘
src                                       └────┘       └────────┘ └─┘          └─┘ 
typ                                      └────┘       └────────┘ └─┘         └─┘
doc                                        └────┘       └────────┘ └─┘          └─┘ 
 39    ∥F.eval x - F.eval y∥ ≤ ∥x - y∥ :=
id     └───┘   └───┘     
src     └───┘     └───┘        
typ    └───┘   └───┘     
doc      └───┘      └───┘
 40  let ⟨z, hz⟩ := F.eval_sub_factor x y in calc
 41    ∥F.eval x - F.eval y∥ = ∥z∥ * ∥x - y∥ : by simp [hz]
src                                               └────┘  └─
typ                                               └────┘  └─
doc                                               └────┘  └─
txt                                               └────┘  └─
par                                               └────┘  └─
pid                                                     
 42      ... ≤ 1 * ∥x - y∥ : mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (norm_nonneg _)
id                           └────────────────────────┘  └─────────────────┘     └─────────┘
src  ───┘                    └────────────────────────┘  └─────────────────┘     └─────────┘
typ  ───┘                    └────────────────────────┘  └─────────────────┘     └─────────┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
 43      ... = ∥x - y∥ : by simp
src                         └────
typ                         └────
doc                         └────
txt                         └────
par                         └────
pid                             
 44  
src  
typ  
doc  
txt  
par  
pid  
 45  open filter metric
 46  
 47  private lemma comp_tendsto_lim {p : ℕ} [p.prime] {F : polynomial ℤ_[p]} (ncs : cau_seq ℤ_[p] norm) :
id                                                                                           └┘ └──┘
src                                                                                          └┘  └──┘
typ                                                                                          └┘ └──┘
doc                                                                                          └┘ 
 48    tendsto (λ i, F.eval (ncs i)) at_top (𝓝 (F.eval ncs.lim)) :=
id     └─────┘      └───┘  └─┘    └────┘    └───┘ └─┘└──┘
src    └─────┘        └───┘          └────┘     └───┘    └──┘
typ    └─────┘      └───┘  └─┘    └────┘    └───┘ └─┘└──┘
doc    └─────┘        └───┘          └────┘     └───┘
 49  (F.continuous_eval.tendsto _).comp ncs.tendsto_limit
 50  
 51  section
 52  parameters {p : ℕ} [nat.prime p] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]} {a : ℤ_[p]}
 53             (ncs_der_val : ∀ n, ∥F.derivative.eval (ncs n)∥ = ∥F.derivative.eval a∥)
 54  include ncs_der_val
 55  
 56  private lemma ncs_tendsto_const :
 57    tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top (𝓝 ∥F.derivative.eval a∥) :=
id                                        └┘    └────┘   └─────────┘└───┘ 
src                                              └────┘    └─────────┘└───┘  
typ                                       └┘    └────┘   └─────────┘└───┘ 
doc                                               └────┘     └─────────┘└───┘
 58  by convert tendsto_const_nhds; ext; rw ncs_der_val
id                            └──┘          └─────────┘
src     └──────┘              └──┘  └─┘  └─┘           
typ     └──────┘              └──┘  └─┘  └─┘└─────────┘
doc     └──────┘                    └─┘  └─┘           
txt     └──────┘                    └─┘  └─┘           
par     └──────┘                    └─┘  └─┘           
pid                                                  
st                            └────────────┘└─────────┘
 59  
src  
typ  
doc  
txt  
par  
pid  
st   
 60  private lemma ncs_tendsto_lim :
 61    tendsto (λ i, ∥F.derivative.eval (ncs i)∥) at_top (𝓝 (∥F.derivative.eval ncs.lim∥)) :=
id     └─────┘      └─────────┘└───┘  └─┘    └────┘    └─────────┘└───┘ └─┘└──┘
src    └─────┘        └─────────┘└───┘          └────┘     └─────────┘└───┘    └──┘
typ    └─────┘      └─────────┘└───┘  └─┘    └────┘    └─────────┘└───┘ └─┘└──┘
doc    └─────┘         └─────────┘└───┘           └────┘      └─────────┘└───┘
 62  tendsto.comp (continuous_iff_continuous_at.1 continuous_norm _) (comp_tendsto_lim _)
id   └──────────┘  └──────────────────────────┘  └─────────────┘     └──────────────┘
src  └──────────┘  └──────────────────────────┘  └─────────────┘     └──────────────┘
typ  └──────────┘  └──────────────────────────┘  └─────────────┘     └──────────────┘
 63  
 64  private lemma norm_deriv_eq : ∥F.derivative.eval ncs.lim∥ = ∥F.derivative.eval a∥ :=
id                                 └─────────┘└───┘ └─┘└──┘  └─────────┘└───┘ 
src                                 └─────────┘└───┘    └──┘   └─────────┘└───┘  
typ                                └─────────┘└───┘ └─┘└──┘  └─────────┘└───┘ 
doc                                  └─────────┘└───┘              └─────────┘└───┘
 65  tendsto_nhds_unique at_top_ne_bot ncs_tendsto_lim ncs_tendsto_const
id   └─────────────────┘ └───────────┘ └─────────────┘ └───────────────┘
src  └─────────────────┘ └───────────┘ └─────────────┘ └───────────────┘
typ  └─────────────────┘ └───────────┘ └─────────────┘ └───────────────┘
 66  
 67  end
 68  
 69  section
 70  parameters {p : ℕ} [nat.prime p] {ncs : cau_seq ℤ_[p] norm} {F : polynomial ℤ_[p]}
id                      └───────┘           └─────┘ └─┘  └──┘       └────────┘ └─┘ 
src                     └───────┘           └─────┘ └─┘  └──┘       └────────┘ └─┘ 
typ                     └───────┘           └─────┘ └─┘  └──┘       └────────┘ └─┘ 
doc                      └───────┘                   └─┘             └────────┘ └─┘ 
 71             (hnorm : tendsto (λ i, ∥F.eval (ncs i)∥) at_top (𝓝 0))
id                       └─────┘       └───┘         └────┘  
src                      └─────┘        └───┘          └────┘  
typ                      └─────┘       └───┘         └────┘  
doc                      └─────┘         └───┘           └────┘  
 72  include hnorm
 73  
 74  private lemma tendsto_zero_of_norm_tendsto_zero : tendsto (λ i, F.eval (ncs i)) at_top (𝓝 0) :=
id                                                     └─────┘      └───┘  └─┘    └────┘  
src                                                    └─────┘        └───┘          └────┘  
typ                                                    └─────┘      └───┘  └─┘    └────┘  
doc                                                    └─────┘        └───┘          └────┘  
 75  tendsto_iff_norm_tendsto_zero.2 (by simpa using hnorm)
id   └───────────────────────────┘                  └───┘
src  └───────────────────────────┘      └──────────┘
typ  └───────────────────────────┘      └──────────┘└───┘
doc                                      └──────────┘
txt                                      └──────────┘
par                                      └──────────┘
pid                                           └────┘
st                                      └────────────────┘
 76  
 77  lemma limit_zero_of_norm_tendsto_zero : F.eval ncs.lim = 0 :=
id                                           └───┘ └─┘└──┘ 
src                                           └───┘    └──┘ 
typ                                          └───┘ └─┘└──┘ 
doc                                           └───┘
 78  tendsto_nhds_unique at_top_ne_bot (comp_tendsto_lim _) tendsto_zero_of_norm_tendsto_zero
id   └─────────────────┘ └───────────┘  └──────────────┘    └───────────────────────────────┘
src  └─────────────────┘ └───────────┘  └──────────────┘    └───────────────────────────────┘
typ  └─────────────────┘ └───────────┘  └──────────────┘    └───────────────────────────────┘
 79  
 80  end
 81  
 82  section hensel
 83  open nat
 84  
 85  parameters {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
id                      └───────┘         └────────┘ └─┘        └─┘ 
src                     └───────┘         └────────┘ └─┘        └─┘ 
typ                     └───────┘         └────────┘ └─┘        └─┘ 
doc                      └───────┘         └────────┘ └─┘        └─┘ 
 86             (hnorm : ∥F.eval a∥ < ∥F.derivative.eval a∥^2) (hnsol : F.eval a ≠ 0)
id                        └───┘     └─────────┘└───┘               └───┘   
src                       └───┘     └─────────┘└───┘               └───┘   
typ                       └───┘     └─────────┘└───┘               └───┘   
doc                        └───┘        └─────────┘└───┘                 └───┘
 87  include hnorm
 88  
 89  /-- `T` is an auxiliary value that is used to control the behavior of the polynomial `F`. -/
 90  private def T : ℝ := ∥(F.eval a).val / ((F.derivative.eval a).val)^2∥
id                        └───┘  └─┘     └─────────┘└───┘  └─┘   
src                        └───┘   └─┘      └─────────┘└───┘   └─┘   
typ                       └───┘  └─┘     └─────────┘└───┘  └─┘   
doc                          └───┘             └─────────┘└───┘
 91  
 92  private lemma deriv_sq_norm_pos : 0 < ∥F.derivative.eval a∥ ^ 2 :=
id                                        └─────────┘└───┘  
src                                        └─────────┘└───┘   
typ                                       └─────────┘└───┘  
doc                                          └─────────┘└───┘
 93  lt_of_le_of_lt (norm_nonneg _) hnorm
id   └────────────┘  └─────────┘    └───┘
src  └────────────┘  └─────────┘
typ  └────────────┘  └─────────┘    └───┘
 94  
 95  private lemma deriv_sq_norm_ne_zero : ∥F.derivative.eval a∥^2 ≠ 0 := ne_of_gt deriv_sq_norm_pos
id                                         └─────────┘└───┘         └──────┘ └───────────────┘
src                                         └─────────┘└───┘          └──────┘ └───────────────┘
typ                                        └─────────┘└───┘         └──────┘ └───────────────┘
doc                                          └─────────┘└───┘
 96  
 97  private lemma deriv_norm_ne_zero : ∥F.derivative.eval a∥ ≠ 0 :=
id                                      └─────────┘└───┘  
src                                      └─────────┘└───┘   
typ                                     └─────────┘└───┘  
doc                                       └─────────┘└───┘
 98  λ h, deriv_sq_norm_ne_zero (by simp [*, _root_.pow_two])
id       └───────────────────┘              └────────────┘
src       └───────────────────┘     └───────┘└────────────┘
typ      └───────────────────┘     └───────┘└────────────┘
doc                                 └───────┘              
txt                                 └───────┘              
par                                 └───────┘              
pid                                     └──┘              
st                                 └───────────────────────┘
 99  
100  private lemma deriv_norm_pos : 0 < ∥F.derivative.eval a∥ :=
id                                     └─────────┘└───┘ 
src                                     └─────────┘└───┘  
typ                                    └─────────┘└───┘ 
doc                                       └─────────┘└───┘
101  lt_of_le_of_ne (norm_nonneg _) (ne.symm deriv_norm_ne_zero)
id   └────────────┘  └─────────┘     └─────┘ └────────────────┘
src  └────────────┘  └─────────┘     └─────┘ └────────────────┘
typ  └────────────┘  └─────────┘     └─────┘ └────────────────┘
102  
103  private lemma deriv_ne_zero : F.derivative.eval a ≠ 0 := mt (norm_eq_zero _).2 deriv_norm_ne_zero
id                                 └─────────┘└───┘        └┘  └──────────┘     └────────────────┘
src                                 └─────────┘└───┘         └┘  └──────────┘     └────────────────┘
typ                                └─────────┘└───┘        └┘  └──────────┘     └────────────────┘
doc                                 └─────────┘└───┘
104  
105  private lemma T_def : T = ∥F.eval a∥ / ∥F.derivative.eval a∥^2 :=
id                           └───┘   └─────────┘└───┘ 
src                           └───┘     └─────────┘└───┘  
typ                          └───┘   └─────────┘└───┘ 
doc                             └───┘        └─────────┘└───┘
106  calc T = ∥(F.eval a).val∥ / ∥((F.derivative.eval a).val)^2∥ : normed_field.norm_div _ _
id            └───┘  └─┘     └─────────┘└───┘  └─┘      └───────────────────┘
src            └───┘   └─┘      └─────────┘└───┘   └─┘      └───────────────────┘
typ           └───┘  └─┘     └─────────┘└───┘  └─┘      └───────────────────┘
doc             └───┘               └─────────┘└───┘
107     ... = ∥F.eval a∥ / ∥(F.derivative.eval a)^2∥ : by simp [norm, padic_norm_z]
id            └───┘    └─────────┘└───┘                     └──────────┘
src            └───┘      └─────────┘└───┘          └────┘    └┘└──────────┘└─
typ           └───┘    └─────────┘└───┘         └────┘    └┘└──────────┘└─
doc             └───┘         └─────────┘└───┘            └────┘    └┘            └─
txt                                                       └────┘    └┘            └─
par                                                       └────┘    └┘            └─
pid                                                               └┘            
st                                                       └──────────────────────────
108     ... = ∥F.eval a∥ / ∥(F.derivative.eval a)∥^2 : by simp [pow, monoid.pow]
id            └───┘    └─────────┘└───┘                    └────────┘
src  ──┘       └───┘      └─────────┘└───┘          └────┘   └┘└────────┘└─
typ  ──┘      └───┘    └─────────┘└───┘         └────┘   └┘└────────┘└─
doc  ──┘        └───┘         └─────────┘└───┘            └────┘   └┘└────────┘└─
txt  ──┘                                                  └────┘   └┘          └─
par  ──┘                                                  └────┘   └┘          └─
pid  ──┘                                                         └┘          
st   ──┘                                                 └───────────────────────
109  
src  
typ  
doc  
txt  
par  
pid  
st   
110  private lemma T_lt_one : T < 1 :=
id                             
src                            
typ                            
doc                           
111  let h := (div_lt_one_iff_lt deriv_sq_norm_pos).2 hnorm in
id            └───────────────┘ └───────────────┘   └───┘
src            └───────────────┘ └───────────────┘ 
typ           └───────────────┘ └───────────────┘   └───┘
112  by rw T_def; apply h
id         └───┘
src     └─┘└───┘  └────┘ 
typ     └─┘└───┘  └────┘ 
doc     └─┘       └────┘ 
txt     └─┘       └────┘ 
par     └─┘       └────┘ 
pid                    
st     └──────────────────
113  
src  
typ  
doc  
txt  
par  
pid  
st   
114  private lemma T_pow {n : ℕ} (hn : n > 0) : T ^ n < 1 :=
id                                              
src                                               
typ                                             
doc                                             
115  have T ^ n ≤ T ^ 1, from pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) (succ_le_of_lt hn),
id                      └──────────────────┘  └─────────┘     └──────┘ └──────┘   └───────────┘ └┘
src                      └──────────────────┘  └─────────┘     └──────┘ └──────┘   └───────────┘
typ                     └──────────────────┘  └─────────┘     └──────┘ └──────┘   └───────────┘ └┘
doc              
116  lt_of_le_of_lt (by simpa) T_lt_one
id   └────────────┘            └──────┘
src  └────────────┘     └───┘  └──────┘
typ  └────────────┘     └───┘  └──────┘
doc                     └───┘
txt                     └───┘
par                     └───┘
st                     └────┘
117  
118  private lemma T_pow' (n : ℕ) : T ^ (2 ^ n) < 1 := (T_pow (nat.pow_pos (by norm_num) _))
id                                                └───┘  └─────────┘
src                                                └───┘  └─────────┘     └──────┘
typ                                               └───┘  └─────────┘     └──────┘
doc                                                                           └──────┘
txt                                                                            └──────┘
par                                                                            └──────┘
st                                                                            └───────┘
119  
120  private lemma T_pow_nonneg (n : ℕ) : T ^ n ≥ 0 := pow_nonneg (norm_nonneg _) _
id                                                └────────┘  └─────────┘
src                                                └────────┘  └─────────┘
typ                                               └────────┘  └─────────┘
doc                                       
121  
122  /-- We will construct a sequence of elements of ℤ_p satisfying successive values of `ih`. -/
123  private def ih (n : ℕ) (z : ℤ_[p]) : Prop :=
id                              └─┘
src                             └─┘ 
typ                             └─┘
doc                              └─┘ 
124  ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧ ∥F.eval z∥ ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n)
id   └─────────┘└───┘   └─────────┘└───┘   └───┘   └─────────┘└───┘        
src   └─────────┘└───┘     └─────────┘└───┘     └───┘     └─────────┘└───┘         
typ  └─────────┘└───┘   └─────────┘└───┘   └───┘   └─────────┘└───┘        
doc    └─────────┘└───┘        └─────────┘└───┘        └───┘        └─────────┘└───┘        
125  
126  private lemma ih_0 : ih 0 a :=
id                        └┘   
src                       └┘
typ                       └┘   
doc                       └┘
127  ⟨ rfl, by simp [T_def, mul_div_cancel' _ (ne_of_gt (deriv_sq_norm_pos hnorm))] ⟩
id     └─┘           └───┘  └─────────────┘    └──────┘  └───────────────┘ └───┘
src    └─┘     └────┘└───┘└┘└─────────────┘└─┘ └──────┘ └───────────────┘     └──┘
typ    └─┘     └────┘└───┘└┘└─────────────┘└─┘ └──────┘ └───────────────┘└───┘└──┘
doc            └────┘     └┘               └─┘                                └──┘
txt            └────┘     └┘               └─┘                                └──┘
par            └────┘     └┘               └─┘                                └──┘
pid                     └┘               └─┘                                └─┘
st            └────────────────────────────────────────────────────────────────────┘
128  
129  private lemma calc_norm_le_one {n : ℕ} {z : ℤ_[p]} (hz : ih n z) :
id                                              └─┘        └┘  
src                                             └─┘         └┘
typ                                             └─┘        └┘  
doc                                              └─┘         └┘
130           ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1 :=
id              └───┘     └─┘    └─────────┘└───┘   
src              └───┘      └─┘      └─────────┘└───┘    
typ             └───┘     └─┘    └─────────┘└───┘   
doc                └───┘      └─┘        └─────────┘└───┘
131  calc ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥
id          └───┘     └─┘    └─────────┘└───┘  
src          └───┘      └─┘      └─────────┘└───┘   
typ         └───┘     └─┘    └─────────┘└───┘  
doc            └───┘      └─┘        └─────────┘└───┘
132      = ∥(↑(F.eval z) : ℚ_[p])∥ / ∥(↑(F.derivative.eval z) : ℚ_[p])∥ : normed_field.norm_div _ _
id           └───┘     └─┘     └─────────┘└───┘     └─┘    └───────────────────┘
src           └───┘      └─┘       └─────────┘└───┘      └─┘     └───────────────────┘
typ          └───┘     └─┘     └─────────┘└───┘     └─┘    └───────────────────┘
doc             └───┘      └─┘           └─────────┘└───┘      └─┘ 
133  ... = ∥F.eval z∥ / ∥F.derivative.eval a∥ : by simp [hz.1]
id         └───┘   └─────────┘└───┘             └┘
src         └───┘     └─────────┘└───┘        └────┘  └──┘
typ        └───┘   └─────────┘└───┘       └────┘└┘└──┘
doc          └───┘        └─────────┘└───┘         └────┘  └──┘
txt                                                └────┘  └──┘
par                                                └────┘  └──┘
pid                                                      └─┘
st                                                └───────────┘
134  ... ≤ ∥F.derivative.eval a∥^2 * T^(2^n) / ∥F.derivative.eval a∥ :
id         └─────────┘└───┘         └─────────┘└───┘ 
src         └─────────┘└───┘            └─────────┘└───┘  
typ        └─────────┘└───┘         └─────────┘└───┘ 
doc          └─────────┘└───┘                   └─────────┘└───┘
135    (div_le_div_right deriv_norm_pos).2 hz.2
id      └──────────────┘ └────────────┘   └┘
src     └──────────────┘ └────────────┘     
typ     └──────────────┘ └────────────┘   └┘
136  ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel (ne_of_gt deriv_norm_pos) _
id         └─────────┘└───┘         └───────────┘  └──────┘ └────────────┘
src         └─────────┘└───┘           └───────────┘  └──────┘ └────────────┘
typ        └─────────┘└───┘         └───────────┘  └──────┘ └────────────┘
doc          └─────────┘└───┘      
137  ... ≤ 1 : mul_le_one (padic_norm_z.le_one _) (T_pow_nonneg _) (le_of_lt (T_pow' _))
id             └────────┘  └─────────────────┘     └──────────┘     └──────┘  └────┘
src            └────────┘  └─────────────────┘     └──────────┘     └──────┘  └────┘
typ            └────────┘  └─────────────────┘     └──────────┘     └──────┘  └────┘
138  
139  private lemma calc_deriv_dist {z z' z1 : ℤ_[p]} (hz' : z' = z - z1)
id                                            └─┘         └┘    └┘
src                                           └─┘                
typ                                           └─┘         └┘    └┘
doc                                           └─┘ 
140    (hz1 : ∥z1∥ = ∥F.eval z∥ / ∥F.derivative.eval a∥) {n} (hz : ih n z) :
id            └┘  └───┘   └─────────┘└───┘             └┘  
src                └───┘     └─────────┘└───┘              └┘
typ           └┘  └───┘   └─────────┘└───┘             └┘  
doc                    └───┘        └─────────┘└───┘               └┘
141    ∥F.derivative.eval z' - F.derivative.eval z∥ < ∥F.derivative.eval a∥ :=
id     └─────────┘└───┘ └┘  └─────────┘└───┘   └─────────┘└───┘ 
src     └─────────┘└───┘      └─────────┘└───┘     └─────────┘└───┘  
typ    └─────────┘└───┘ └┘  └─────────┘└───┘   └─────────┘└───┘ 
doc      └─────────┘└───┘       └─────────┘└───┘        └─────────┘└───┘
142  calc
143    ∥F.derivative.eval z' - F.derivative.eval z∥
id     └─────────┘└───┘ └┘  └─────────┘└───┘ 
src     └─────────┘└───┘      └─────────┘└───┘  
typ    └─────────┘└───┘ └┘  └─────────┘└───┘ 
doc      └─────────┘└───┘       └─────────┘└───┘
144      ≤ ∥z' - z∥ : padic_polynomial_dist _ _ _
id         └┘     └───────────────────┘
src                └───────────────────┘
typ        └┘     └───────────────────┘
145  ... = ∥z1∥ : by simp [hz']
id         └┘            └─┘
src                └────┘   └┘
typ        └┘      └────┘└─┘└┘
doc                  └────┘   └┘
txt                  └────┘   └┘
par                  └────┘   └┘
pid                         
st                  └──────────┘
146  ... = ∥F.eval z∥ / ∥F.derivative.eval a∥ : hz1
id         └───┘   └─────────┘└───┘    └─┘
src         └───┘     └─────────┘└───┘  
typ        └───┘   └─────────┘└───┘    └─┘
doc          └───┘        └─────────┘└───┘
147  ... ≤ ∥F.derivative.eval a∥^2 * T^(2^n) / ∥F.derivative.eval a∥ : (div_le_div_right deriv_norm_pos).2 hz.2
id         └─────────┘└───┘         └─────────┘└───┘     └──────────────┘ └────────────┘   └┘
src         └─────────┘└───┘            └─────────┘└───┘      └──────────────┘ └────────────┘     
typ        └─────────┘└───┘         └─────────┘└───┘     └──────────────┘ └────────────┘   └┘
doc          └─────────┘└───┘                   └─────────┘└───┘
148  ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel deriv_norm_ne_zero _
id         └─────────┘└───┘         └───────────┘ └────────────────┘
src         └─────────┘└───┘           └───────────┘ └────────────────┘
typ        └─────────┘└───┘         └───────────┘ └────────────────┘
doc          └─────────┘└───┘      
149  ... < ∥F.derivative.eval a∥ : (mul_lt_iff_lt_one_right deriv_norm_pos).2 (T_pow (pow_pos (by norm_num) _))
id         └─────────┘└───┘     └─────────────────────┘ └────────────┘    └───┘  └─────┘
src         └─────────┘└───┘      └─────────────────────┘ └────────────┘    └───┘  └─────┘     └──────┘
typ        └─────────┘└───┘     └─────────────────────┘ └────────────┘    └───┘  └─────┘     └──────┘
doc          └─────────┘└───┘                                                                     └──────┘
txt                                                                                               └──────┘
par                                                                                               └──────┘
st                                                                                               └───────┘
150  
151  private def calc_eval_z'  {z z' z1 : ℤ_[p]} (hz' : z' = z - z1) {n} (hz : ih n z)
id                                        └─┘         └┘    └┘            └┘  
src                                       └─┘                               └┘
typ                                       └─┘         └┘    └┘            └┘  
doc                                       └─┘                                 └┘
152    (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1) (hzeq : z1 = ⟨_, h1⟩) :
id             └───┘     └─┘    └─────────┘└───┘               └┘      └┘
src             └───┘      └─┘      └─────────┘└───┘                   
typ            └───┘     └─┘    └─────────┘└───┘               └┘      └┘
doc               └───┘      └─┘        └─────────┘└───┘
153    {q : ℤ_[p] // F.eval z' = q * z1^2} :=
id         └─┘    └───┘ └┘    └┘
src        └─┘      └───┘          
typ        └─┘    └───┘ └┘    └┘
doc         └─┘      └───┘
154  have hdzne' : (↑(F.derivative.eval z) : ℚ_[p]) ≠ 0, from
id                   └─────────┘└───┘     └─┘  
src                   └─────────┘└───┘      └─┘   
typ                  └─────────┘└───┘     └─┘  
doc                    └─────────┘└───┘      └─┘ 
155    have hdzne : F.derivative.eval z ≠ 0,
id                  └─────────┘└───┘  
src                  └─────────┘└───┘   
typ                 └─────────┘└───┘  
doc                  └─────────┘└───┘
156      from mt (norm_eq_zero _).2 (by rw hz.1; apply deriv_norm_ne_zero; assumption),
id            └┘  └──────────┘            └┘          └────────────────┘
src           └┘  └──────────┘         └─┘  └┘  └────┘└────────────────┘  └────────┘
typ           └┘  └──────────┘         └─┘└┘└┘  └────┘└────────────────┘  └────────┘
doc                                     └─┘  └┘  └────┘                    └────────┘
txt                                     └─┘  └┘  └────┘                    └────────┘
par                                     └─┘  └┘  └────┘                    └────────┘
pid                                         └┘       
st                                     └────────────────────────────────────────────┘
157    λ h, hdzne $ subtype.ext.2 h,
id         └───┘   └─────────┘  
src                 └─────────┘
typ        └───┘   └─────────┘  
158  let ⟨q, hq⟩ := F.binom_expansion z (-z1) in
id   └─┘           └──────────────┘   └┘
src                  └──────────────┘    
typ  └─┘           └──────────────┘   └┘
159  have ∥(↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)) : ℚ_[p])∥ ≤ 1,
id          └─────────┘└───┘      └───┘     └─────────┘└───┘      └─┘  
src          └─────────┘└───┘        └───┘       └─────────┘└───┘       └─┘   
typ         └─────────┘└───┘      └───┘     └─────────┘└───┘      └─┘  
doc            └─────────┘└───┘          └───┘         └─────────┘└───┘       └─┘ 
160    by {rw padic_norm_e.mul, apply mul_le_one, apply padic_norm_z.le_one, apply norm_nonneg, apply h1},
id            └──────────────┘        └────────┘        └─────────────────┘        └─────────┘
src        └─┘└──────────────┘  └────┘└────────┘  └────┘└─────────────────┘  └────┘└─────────┘  └────┘
typ        └─┘└──────────────┘  └────┘└────────┘  └────┘└─────────────────┘  └────┘└─────────┘  └────┘
doc        └─┘                  └────┘            └────┘                     └────┘             └────┘
txt        └─┘                  └────┘            └────┘                     └────┘             └────┘
par        └─┘                  └────┘            └────┘                     └────┘             └────┘
pid                                                                                              
st       └───────────────────┘└────────────────┘└─────────────────────────┘└─────────────────┘└────────┘└┘
161  have F.derivative.eval z * (-z1) = -F.eval z, from calc
id        └─────────┘└───┘    └┘   └───┘ 
src        └─────────┘└───┘           └───┘
typ       └─────────┘└───┘    └┘   └───┘ 
doc        └─────────┘└───┘               └───┘
162    F.derivative.eval z * (-z1)
id     └─────────┘└───┘    └┘
src     └─────────┘└───┘     
typ    └─────────┘└───┘    └┘
doc     └─────────┘└───┘
163      = (F.derivative.eval z) * -⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩ : by rw [hzeq]
id          └─────────┘└───┘      └───┘     └─────────┘└───┘    └┘           └──┘
src          └─────────┘└───┘        └───┘       └─────────┘└───┘              └──┘    └┘
typ         └─────────┘└───┘      └───┘     └─────────┘└───┘    └┘       └──┘└──┘└┘
doc          └─────────┘└───┘           └───┘         └─────────┘└───┘              └──┘    └┘
txt                                                                                 └──┘    └┘
par                                                                                 └──┘    └┘
pid                                                                                   └┘    
st                                                                                 └───────┘
164  ... = -((F.derivative.eval z) * ⟨↑(F.eval z) / ↑(F.derivative.eval z), h1⟩) : by simp
id           └─────────┘└───┘      └───┘     └─────────┘└───┘    └┘
src           └─────────┘└───┘        └───┘       └─────────┘└───┘               └───┘
typ          └─────────┘└───┘      └───┘     └─────────┘└───┘    └┘        └───┘
doc            └─────────┘└───┘          └───┘         └─────────┘└───┘               └───┘
txt                                                                                   └───┘
par                                                                                   └───┘
pid                                                                                       
st                                                                                   └────┘
165  ... = -(⟨↑(F.derivative.eval z) * (↑(F.eval z) / ↑(F.derivative.eval z)), this⟩) : subtype.ext.2 $ by simp
id            └─────────┘└───┘      └───┘     └─────────┘└───┘     └──┘     └─────────┘
src            └─────────┘└───┘        └───┘       └─────────┘└───┘               └─────────┘       └───┘
typ           └─────────┘└───┘      └───┘     └─────────┘└───┘     └──┘     └─────────┘       └───┘
doc              └─────────┘└───┘          └───┘         └─────────┘└───┘                                  └───┘
txt                                                                                                        └───┘
par                                                                                                        └───┘
pid                                                                                                            
st                                                                                                        └────┘
166  ... = -(F.eval z) : by simp [mul_div_cancel' _ hdzne'],
id          └───┘              └─────────────┘   └────┘
src          └───┘         └────┘└─────────────┘└─┘      
typ         └───┘        └────┘└─────────────┘└─┘└────┘
doc           └───┘         └────┘               └─┘      
txt                         └────┘               └─┘      
par                         └────┘               └─┘      
pid                                            └─┘      
st                         └──────────────────────────────┘
167  have heq : F.eval z' = q * z1^2, by simpa [this, hz'] using hq,
id              └───┘ └┘     └┘             └──┘  └─┘        └┘
src              └───┘                └─────┘    └┘   └──────┘
typ             └───┘ └┘     └┘      └─────┘└──┘└┘└─┘└──────┘└┘
doc              └───┘                   └─────┘    └┘   └──────┘
txt                                      └─────┘    └┘   └──────┘
par                                      └─────┘    └┘   └──────┘
pid                                               └┘   └────┘
st                                      └─────────────────────────┘
168  ⟨q, heq⟩
id       └─┘
src      └─┘
typ      └─┘
169  
170  private def calc_eval_z'_norm {z z' z1 : ℤ_[p]} {n} (hz : ih n z) {q}
id                                            └─┘            └┘  
src                                           └─┘             └┘
typ                                           └─┘            └┘  
doc                                           └─┘             └┘
171    (heq : F.eval z' = q * z1^2) (h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1)
id            └───┘ └┘    └┘           └───┘     └─┘    └─────────┘└───┘   
src            └───┘                      └───┘      └─┘      └─────────┘└───┘    
typ           └───┘ └┘    └┘           └───┘     └─┘    └─────────┘└───┘   
doc            └───┘                           └───┘      └─┘        └─────────┘└───┘
172    (hzeq : z1 = ⟨_, h1⟩) : ∥F.eval z'∥ ≤ ∥F.derivative.eval a∥^2 * T^(2^(n+1)) :=
id             └┘      └┘     └───┘ └┘  └─────────┘└───┘       
src                            └───┘      └─────────┘└───┘         
typ            └┘      └┘     └───┘ └┘  └─────────┘└───┘       
doc                              └───┘         └─────────┘└───┘        
173  calc ∥F.eval z'∥
id        └───┘ └┘
src        └───┘   
typ       └───┘ └┘
doc         └───┘
174      = ∥q∥ * ∥z1∥^2 : by simp [heq]
id           └┘             └─┘
src                    └────┘└─┘└┘
typ          └┘       └────┘└─┘└┘
doc                          └────┘   └┘
txt                          └────┘   └┘
par                          └────┘   └┘
pid                                 
st                          └──────────┘
175  ... ≤ 1 * ∥z1∥^2 : mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (pow_nonneg (norm_nonneg _) _)
id            └┘    └────────────────────────┘  └─────────────────┘     └────────┘  └─────────┘
src                 └────────────────────────┘  └─────────────────┘     └────────┘  └─────────┘
typ           └┘    └────────────────────────┘  └─────────────────┘     └────────┘  └─────────┘
176  ... = ∥F.eval z∥^2 / ∥F.derivative.eval a∥^2 :
id         └───┘    └─────────┘└───┘ 
src         └───┘      └─────────┘└───┘  
typ        └───┘    └─────────┘└───┘ 
doc          └───┘          └─────────┘└───┘
177    by simp [hzeq, hz.1, div_pow _ (deriv_norm_ne_zero hnorm)]
id              └──┘  └┘    └─────┘    └────────────────┘ └───┘
src       └────┘    └┘  └──┘└─────┘└─┘ └────────────────┘     └─┘
typ       └────┘└──┘└┘└┘└──┘└─────┘└─┘ └────────────────┘└───┘└─┘
doc       └────┘    └┘  └──┘       └─┘                        └─┘
txt       └────┘    └┘  └──┘       └─┘                        └─┘
par       └────┘    └┘  └──┘       └─┘                        └─┘
pid               └┘  └──┘       └─┘                        └┘
st       └───────────────────────────────────────────────────────┘
178  ... ≤ (∥F.derivative.eval a∥^2 * T^(2^n))^2 / ∥F.derivative.eval a∥^2 :
id          └─────────┘└───┘           └─────────┘└───┘ 
src          └─────────┘└───┘              └─────────┘└───┘  
typ         └─────────┘└───┘           └─────────┘└───┘ 
doc           └─────────┘└───┘                      └─────────┘└───┘
179    (div_le_div_right deriv_sq_norm_pos).2 (pow_le_pow_of_le_left (norm_nonneg _) hz.2 _)
id      └──────────────┘ └───────────────┘    └───────────────────┘  └─────────┘    └┘
src     └──────────────┘ └───────────────┘    └───────────────────┘  └─────────┘      
typ     └──────────────┘ └───────────────┘    └───────────────────┘  └─────────┘    └┘
180  ... = (∥F.derivative.eval a∥^2)^2 * (T^(2^n))^2 / ∥F.derivative.eval a∥^2 : by simp only [_root_.mul_pow]
id          └─────────┘└───┘              └─────────┘└───┘                   └────────────┘
src          └─────────┘└───┘                 └─────────┘└───┘         └─────────┘└────────────┘└┘
typ         └─────────┘└───┘              └─────────┘└───┘        └─────────┘└────────────┘└┘
doc           └─────────┘└───┘                          └─────────┘└───┘           └─────────┘              └┘
txt                                                                                 └─────────┘              └┘
par                                                                                 └─────────┘              └┘
pid                                                                                     └──┘└┘              
st                                                                                 └──────────────────────────┘
181  ... = ∥F.derivative.eval a∥^2 * (T^(2^n))^2 : div_sq_cancel deriv_sq_norm_ne_zero _
id         └─────────┘└───┘             └───────────┘ └───────────────────┘
src         └─────────┘└───┘               └───────────┘ └───────────────────┘
typ        └─────────┘└───┘             └───────────┘ └───────────────────┘
doc          └─────────┘└───┘         
182  ... = ∥F.derivative.eval a∥^2 * T^(2^(n + 1)) : by rw [←pow_mul]; refl
id         └─────────┘└───┘                       └─────┘
src         └─────────┘└───┘                    └───┘└─────┘  └────
typ        └─────────┘└───┘                  └───┘└─────┘  └────
doc          └─────────┘└───┘                          └───┘         └────
txt                                                     └───┘         └────
par                                                     └───┘         └────
pid                                                       └─┘             
st                                                     └───────────┘└──────
183  
src  
typ  
doc  
txt  
par  
pid  
st   
184  set_option eqn_compiler.zeta true
doc             └───────────────┘
185  
186  /-- Given `z : ℤ_[p]` satisfying `ih n z`, construct `z' : ℤ_[p]` satisfying `ih (n+1) z'`. We need
187  the hypothesis `ih n z`, since otherwise `z'` is not necessarily an integer. -/
188  private def ih_n {n : ℕ} {z : ℤ_[p]} (hz : ih n z) : {z' : ℤ_[p] // ih (n+1) z'} :=
id                                └─┘        └┘           └─┘    └┘     └┘
src                               └─┘         └┘             └─┘     └┘   
typ                               └─┘        └┘           └─┘    └┘     └┘
doc                                └─┘         └┘              └─┘     └┘
189  have h1 : ∥(↑(F.eval z) : ℚ_[p]) / ↑(F.derivative.eval z)∥ ≤ 1, from calc_norm_le_one hz,
id               └───┘     └─┘    └─────────┘└───┘            └──────────────┘ └┘
src               └───┘      └─┘      └─────────┘└───┘             └──────────────┘
typ              └───┘     └─┘    └─────────┘└───┘            └──────────────┘ └┘
doc                 └───┘      └─┘        └─────────┘└───┘
190  let z1 : ℤ_[p] := ⟨_, h1⟩,
id            └─┘        └┘
src           └─┘ 
typ           └─┘        └┘
doc           └─┘ 
191      z' : ℤ_[p] := z - z1 in
id            └─┘      └┘
src           └─┘       
typ           └─┘      └┘
doc           └─┘ 
192  ⟨ z',
id     └┘
typ    └┘
193    have hdist : ∥F.derivative.eval z' - F.derivative.eval z∥ < ∥F.derivative.eval a∥,
id                  └─────────┘└───┘ └┘  └─────────┘└───┘   └─────────┘└───┘ 
src                  └─────────┘└───┘      └─────────┘└───┘     └─────────┘└───┘  
typ                 └─────────┘└───┘ └┘  └─────────┘└───┘   └─────────┘└───┘ 
doc                   └─────────┘└───┘       └─────────┘└───┘        └─────────┘└───┘
194      from calc_deriv_dist rfl (by simp [z1, hz.1]) hz,
id            └─────────────┘ └─┘           └┘  └┘     └┘
src           └─────────────┘ └─┘     └────┘  └┘  └─┘
typ           └─────────────┘ └─┘     └────┘└┘└┘└┘└─┘  └┘
doc                                   └────┘  └┘  └─┘
txt                                   └────┘  └┘  └─┘
par                                   └────┘  └┘  └─┘
pid                                         └┘  └─┘
st                                   └──────────────┘
195    have hfeq : ∥F.derivative.eval z'∥ = ∥F.derivative.eval a∥,
id                 └─────────┘└───┘ └┘  └─────────┘└───┘ 
src                 └─────────┘└───┘      └─────────┘└───┘  
typ                └─────────┘└───┘ └┘  └─────────┘└───┘ 
doc                  └─────────┘└───┘         └─────────┘└───┘
196      begin
st       └─────
197        rw [sub_eq_add_neg, ← hz.1, ←norm_neg (F.derivative.eval z)] at hdist,
id             └────────────┘    └┘     └──────┘  └───────────────┘ 
src        └──┘└────────────┘└──┘  └───┘└──────┘ └───────────────┘ └─────────┘
typ        └──┘└────────────┘└──┘└┘└───┘└──────┘ └───────────────┘└─────────┘
doc        └──┘              └──┘  └───┘         └───────────────┘ └─────────┘
txt        └──┘              └──┘  └───┘                           └─────────┘
par        └──┘              └──┘  └───┘                           └─────────┘
pid          └┘              └──┘  └───┘                           └┘└───────┘
st   ───────────────────────┘└────┘└─────────────────────────────────┘└───────┘└─
198        have := padic_norm_z.eq_of_norm_add_lt_right hdist,
id                 └──────────────────────────────────┘ └───┘
src        └──────┘└──────────────────────────────────┘
typ        └──────┘└──────────────────────────────────┘└───┘
doc        └──────┘                                    
txt        └──────┘                                    
par        └──────┘                                    
pid        └───┘└─┘                                    
st   ───────────────────────────────────────────────────────┘└─
199        rwa [norm_neg, hz.1] at this
id              └──────┘  └┘
src        └───┘└──────┘└┘  └───────────
typ        └───┘└──────┘└┘└┘└───────────
doc        └───┘        └┘  └───────────
txt        └───┘        └┘  └───────────
par        └───┘        └┘  └───────────
pid           └┘        └┘  └─┘└──────┘
st   ──────────────────┘└──┘└─┘└────────
200      end,
src  ───┘
typ  ───┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘└─┘
201    let ⟨q, heq⟩ := calc_eval_z' rfl hz h1 rfl in
id     └─┘     └─┘     └──────────┘ └─┘ └┘ └┘ └─┘
src            └─┘     └──────────┘ └─┘       └─┘
typ    └─┘     └─┘     └──────────┘ └─┘ └┘ └┘ └─┘
202    have hnle : ∥F.eval z'∥ ≤ ∥F.derivative.eval a∥^2 * T^(2^(n+1)),
id                 └───┘ └┘  └─────────┘└───┘       
src                 └───┘      └─────────┘└───┘         
typ                └───┘ └┘  └─────────┘└───┘       
doc                  └───┘         └─────────┘└───┘        
203      from calc_eval_z'_norm hz heq h1 rfl,
id            └───────────────┘ └┘     └┘ └─┘
src           └───────────────┘           └─┘
typ           └───────────────┘ └┘     └┘ └─┘
204    ⟨hfeq, hnle⟩⟩
id      └──┘  └──┘
typ     └──┘  └──┘
205  
206  set_option eqn_compiler.zeta false
doc             └───────────────┘
207  
208  -- why doesn't "noncomputable theory" stick here?
209  private noncomputable def newton_seq_aux : Π n : ℕ, {z : ℤ_[p] // ih n z}
id                                                         └─┘    └┘  
src                                                         └─┘     └┘
typ                                                        └─┘    └┘  
doc                                                           └─┘     └┘
210  | 0 := ⟨a, ih_0⟩
id             └──┘
src             └──┘
typ            └──┘
211  | (k+1) := ih_n (newton_seq_aux k).2
id            └──┘  └────────────┘   
src            └──┘                   
typ           └──┘  └────────────┘   
doc             └──┘
212  
213  private def newton_seq (n : ℕ) : ℤ_[p] := (newton_seq_aux n).1
id                                   └─┘     └────────────┘  
src                                  └─┘      └────────────┘   
typ                                  └─┘     └────────────┘  
doc                                   └─┘ 
214  
215  private lemma newton_seq_deriv_norm (n : ℕ) :
id                                            
src                                           
typ                                           
216    ∥F.derivative.eval (newton_seq n)∥ = ∥F.derivative.eval a∥ :=
id     └─────────┘└───┘  └────────┘    └─────────┘└───┘ 
src     └─────────┘└───┘  └────────┘      └─────────┘└───┘  
typ    └─────────┘└───┘  └────────┘    └─────────┘└───┘ 
doc      └─────────┘└───┘                     └─────────┘└───┘
217  (newton_seq_aux n).2.1
id    └────────────┘   
src   └────────────┘    
typ   └────────────┘   
218  
219  private lemma newton_seq_norm_le (n : ℕ) :
id                                         
src                                        
typ                                        
220    ∥F.eval (newton_seq n)∥ ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n) :=
id     └───┘  └────────┘    └─────────┘└───┘        
src     └───┘  └────────┘      └─────────┘└───┘         
typ    └───┘  └────────┘    └─────────┘└───┘        
doc      └───┘                     └─────────┘└───┘        
221  (newton_seq_aux n).2.2
id    └────────────┘   
src   └────────────┘    
typ   └────────────┘   
222  
223  private lemma newton_seq_norm_eq (n : ℕ) :
id                                         
src                                        
typ                                        
224    ∥newton_seq (n+1) - newton_seq n∥ = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ :=
id     └────────┘      └────────┘   └───┘  └────────┘    └─────────┘└───┘  └────────┘  
src    └────────┘       └────────┘     └───┘  └────────┘      └─────────┘└───┘  └────────┘   
typ    └────────┘      └────────┘   └───┘  └────────┘    └─────────┘└───┘  └────────┘  
doc                                          └───┘                     └─────────┘└───┘
225  by induction n; simp [newton_seq, newton_seq_aux, ih_n]
id                        └────────┘  └────────────┘  └──┘
src     └────────┘   └────┘└────────┘└┘└────────────┘└┘└──┘└─
typ     └────────┘  └────┘└────────┘└┘└────────────┘└┘└──┘└─
doc     └────────┘   └────┘          └┘              └┘└──┘└─
txt     └────────┘   └────┘          └┘              └┘    └─
par     └────────┘   └────┘          └┘              └┘    └─
pid                               └┘              └┘    
st     └─────────────────────────────────────────────────────
226  
src  
typ  
doc  
txt  
par  
pid  
st   
227  private lemma newton_seq_succ_dist (n : ℕ) :
id                                           
src                                          
typ                                          
228    ∥newton_seq (n+1) - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=
id     └────────┘      └────────┘   └─────────┘└───┘     
src    └────────┘       └────────┘     └─────────┘└───┘      
typ    └────────┘      └────────┘   └─────────┘└───┘     
doc                                          └─────────┘└───┘      
229  calc ∥newton_seq (n+1) - newton_seq n∥
id        └────────┘      └────────┘ 
src       └────────┘       └────────┘  
typ       └────────┘      └────────┘ 
230      = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval (newton_seq n)∥ : newton_seq_norm_eq _
id         └───┘  └────────┘    └─────────┘└───┘  └────────┘     └────────────────┘
src         └───┘  └────────┘      └─────────┘└───┘  └────────┘      └────────────────┘
typ        └───┘  └────────┘    └─────────┘└───┘  └────────┘     └────────────────┘
doc          └───┘                     └─────────┘└───┘
231  ... = ∥F.eval (newton_seq n)∥ / ∥F.derivative.eval a∥ : by rw newton_seq_deriv_norm
id         └───┘  └────────┘    └─────────┘└───┘          └───────────────────┘
src         └───┘  └────────┘      └─────────┘└───┘        └─┘└───────────────────┘
typ        └───┘  └────────┘    └─────────┘└───┘       └─┘└───────────────────┘
doc          └───┘                     └─────────┘└───┘         └─┘                     
txt                                                             └─┘                     
par                                                             └─┘                     
pid                                                                                    
st                                                             └────────────────────────┘
232  ... ≤ ∥F.derivative.eval a∥^2 * T ^ (2^n) / ∥F.derivative.eval a∥ :
id         └─────────┘└───┘           └─────────┘└───┘ 
src         └─────────┘└───┘              └─────────┘└───┘  
typ        └─────────┘└───┘           └─────────┘└───┘ 
doc          └─────────┘└───┘                     └─────────┘└───┘
233    (div_le_div_right deriv_norm_pos).2 (newton_seq_norm_le _)
id      └──────────────┘ └────────────┘    └────────────────┘
src     └──────────────┘ └────────────┘    └────────────────┘
typ     └──────────────┘ └────────────┘    └────────────────┘
234  ... = ∥F.derivative.eval a∥ * T^(2^n) : div_sq_cancel (ne_of_gt deriv_norm_pos) _
id         └─────────┘└───┘         └───────────┘  └──────┘ └────────────┘
src         └─────────┘└───┘           └───────────┘  └──────┘ └────────────┘
typ        └─────────┘└───┘         └───────────┘  └──────┘ └────────────┘
doc          └─────────┘└───┘      
235  
236  include hnsol
237  private lemma T_pos : T > 0 :=
id                          
src                         
typ                         
doc                        
238  begin
st   └─────
239    rw T_def,
id        └───┘
src    └─┘└───┘
typ    └─┘└───┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────┘└─
240    apply div_pos_of_pos_of_pos,
id           └───────────────────┘
src    └────┘└───────────────────┘
typ    └────┘└───────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────────┘└─
241    { apply (norm_pos_iff _).2,
id              └──────────┘
src      └────┘ └──────────┘└───┘
typ      └────┘ └──────────┘└───┘
doc      └────┘             └───┘
txt      └────┘             └───┘
par      └────┘             └───┘
pid                        └─┘└┘
st   ───┘└──────────────────────┘└─
242      apply hnsol },
src      └────┘     
typ      └────┘     
doc      └────┘     
txt      └────┘     
par      └────┘     
pid                
st   ───────────────┘└┘
243    { exact deriv_sq_norm_pos hnorm }
id             └───────────────┘ └───┘
src      └────┘└───────────────┘     
typ      └────┘└───────────────┘└───┘
doc      └────┘                      
txt      └────┘                      
par      └────┘                      
pid                                 
st   ─────────────────────────────────┘└─
244  end
st   ──┘
245  
246  private lemma newton_seq_succ_dist_weak (n : ℕ) :
id                                                
src                                               
typ                                               
247    ∥newton_seq (n+2) - newton_seq (n+1)∥ < ∥F.eval a∥ / ∥F.derivative.eval a∥ :=
id     └────────┘      └────────┘      └───┘   └─────────┘└───┘ 
src    └────────┘       └────────┘        └───┘     └─────────┘└───┘  
typ    └────────┘      └────────┘      └───┘   └─────────┘└───┘ 
doc                                              └───┘        └─────────┘└───┘
248  have 2 ≤ 2^(n+1),
id             
src             
typ            
249    from have _, from pow_le_pow (by norm_num : 1 ≤ 2) (nat.le_add_left _ _ : 1 ≤ n + 1),
id                       └────────┘                       └─────────────┘           
src                      └────────┘     └───────┘         └─────────────┘            
typ                      └────────┘     └───────┘         └─────────────┘           
doc                                     └───────┘
txt                                     └───────┘
par                                     └───────┘
pid                                             
st                                     └────────┘
250      by simpa using this,
id                      └──┘
src         └──────────┘
typ         └──────────┘└──┘
doc         └──────────┘
txt         └──────────┘
par         └──────────┘
pid              └────┘
st         └───────────────┘
251  calc ∥newton_seq (n+2) - newton_seq (n+1)∥
id        └────────┘      └────────┘    
src       └────────┘       └────────┘     
typ       └────────┘      └────────┘    
252      ≤ ∥F.derivative.eval a∥ * T^(2^(n+1)) : newton_seq_succ_dist _
id         └─────────┘└───┘            └──────────────────┘
src         └─────────┘└───┘              └──────────────────┘
typ        └─────────┘└───┘            └──────────────────┘
doc          └─────────┘└───┘      
253  ... ≤ ∥F.derivative.eval a∥ * T^2 : mul_le_mul_of_nonneg_left
id         └─────────┘└───┘       └───────────────────────┘
src         └─────────┘└───┘        └───────────────────────┘
typ        └─────────┘└───┘       └───────────────────────┘
doc          └─────────┘└───┘      
254                                        (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this)
id                                          └──────────────────┘  └─────────┘     └──────┘ └──────┘  └──┘
src                                         └──────────────────┘  └─────────┘     └──────┘ └──────┘
typ                                         └──────────────────┘  └─────────┘     └──────┘ └──────┘  └──┘
255                                        (norm_nonneg _)
id                                          └─────────┘
src                                         └─────────┘
typ                                         └─────────┘
256  ... < ∥F.derivative.eval a∥ * T^1 : mul_lt_mul_of_pos_left (pow_lt_pow_of_lt_one T_pos T_lt_one (by norm_num))
id         └─────────┘└───┘       └────────────────────┘  └──────────────────┘ └───┘ └──────┘
src         └─────────┘└───┘        └────────────────────┘  └──────────────────┘ └───┘ └──────┘     └──────┘
typ        └─────────┘└───┘       └────────────────────┘  └──────────────────┘ └───┘ └──────┘     └──────┘
doc          └─────────┘└───┘                                                                           └──────┘
txt                                                                                                      └──────┘
par                                                                                                      └──────┘
st                                                                                                      └───────┘
257                                                             deriv_norm_pos
id                                                              └────────────┘
src                                                             └────────────┘
typ                                                             └────────────┘
258  ... = ∥F.eval a∥ / ∥F.derivative.eval a∥ :
id         └───┘   └─────────┘└───┘ 
src         └───┘     └─────────┘└───┘  
typ        └───┘   └─────────┘└───┘ 
doc          └───┘        └─────────┘└───┘
259    begin
st     └─────
260      rw [T, _root_.pow_two, _root_.pow_one, normed_field.norm_div, ←mul_div_assoc, padic_norm_e.mul],
id             └────────────┘  └────────────┘  └───────────────────┘   └───────────┘  └──────────────┘
src      └──┘└┘└────────────┘└┘└────────────┘└┘└───────────────────┘└─┘└───────────┘└┘└──────────────┘
typ      └──┘└┘└────────────┘└┘└────────────┘└┘└───────────────────┘└─┘└───────────┘└┘└──────────────┘
doc      └──┘└┘              └┘              └┘                     └─┘             └┘                
txt      └──┘ └┘              └┘              └┘                     └─┘             └┘                
par      └──┘ └┘              └┘              └┘                     └─┘             └┘                
pid        └┘ └┘              └┘              └┘                     └─┘             └┘                
st   ────────┘└──────────────┘└──────────────┘└─────────────────────┘└──────────────┘└────────────────┘└──
261      apply mul_div_mul_left',
id             └───────────────┘
src      └────┘└───────────────┘
typ      └────┘└───────────────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ──────────────────────────┘└─
262      apply deriv_norm_ne_zero; assumption
id             └────────────────┘
src      └────┘└────────────────┘  └──────────
typ      └────┘└────────────────┘  └──────────
doc      └────┘                    └──────────
txt      └────┘                    └──────────
par      └────┘                    └──────────
pid                                         
st   ─────────────────────────────────────────
263    end
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
264  
265  private lemma newton_seq_dist_aux (n : ℕ) :
id                                          
src                                         
typ                                         
266    ∀ k : ℕ, ∥newton_seq (n + k) - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n)
id            └────────┘       └────────┘   └─────────┘└───┘     
src            └────────┘         └────────┘     └─────────┘└───┘      
typ           └────────┘       └────────┘   └─────────┘└───┘     
doc                                                     └─────────┘└───┘      
267  | 0 := begin simp, apply mul_nonneg, {apply norm_nonneg}, {apply T_pow_nonneg} end
id                            └────────┘         └─────────┘          └──────────┘
src               └──┘  └────┘└────────┘   └────┘└─────────┘    └────┘└──────────┘
typ               └──┘  └────┘└────────┘   └────┘└─────────┘    └────┘└──────────┘
doc               └──┘  └────┘             └────┘               └────┘
txt               └──┘  └────┘             └────┘               └────┘
par               └──┘  └────┘             └────┘               └────┘
pid                                                                
st          └────────┘└────────────────┘└──────────────────┘└┘└──────────────────┘└───┘
268  | (k+1) :=
id      
src      
typ     
269    have 2^n ≤ 2^(n+k),
id               
src                
typ              
270      by {rw [←nat.pow_eq_pow, ←nat.pow_eq_pow], apply pow_le_pow, norm_num, apply nat.le_add_right},
id                └────────────┘   └────────────┘         └────────┘                  └──────────────┘
src          └───┘└────────────┘└─┘└────────────┘  └────┘└────────┘  └──────┘  └────┘└──────────────┘
typ          └───┘└────────────┘└─┘└────────────┘  └────┘└────────┘  └──────┘  └────┘└──────────────┘
doc          └───┘              └─┘                └────┘            └──────┘  └────┘
txt          └───┘              └─┘                └────┘            └──────┘  └────┘
par          └───┘              └─┘                └────┘            └──────┘  └────┘
pid            └─┘              └─┘                                                
st         └───────────────────┘└───────────────┘└─────────────────┘└────────┘└──────────────────────┘└┘
271    calc
272    ∥newton_seq (n + (k + 1)) - newton_seq n∥
id     └────────┘             └────────┘ 
src    └────────┘              └────────┘  
typ    └────────┘             └────────┘ 
273      = ∥newton_seq ((n + k) + 1) - newton_seq n∥ : by simp
id         └────────┘             └────────┘ 
src        └────────┘              └────────┘        └───┘
typ        └────────┘             └────────┘       └───┘
doc                                                       └───┘
txt                                                       └───┘
par                                                       └───┘
pid                                                           
st                                                       └────┘
274  ... = ∥(newton_seq ((n + k) + 1) - newton_seq (n+k)) + (newton_seq (n+k) - newton_seq n)∥ : by rw ←sub_add_sub_cancel
id          └────────┘             └────────┘        └────────┘      └────────┘            └────────────────┘
src         └────────┘              └────────┘         └────────┘       └────────┘         └──┘└────────────────┘
typ         └────────┘             └────────┘        └────────┘      └────────┘        └──┘└────────────────┘
doc                                                                                                 └──┘                  
txt                                                                                                 └──┘                  
par                                                                                                 └──┘                  
pid                                                                                                   └┘                  
st                                                                                                 └──────────────────────┘
275  ... ≤ max (∥newton_seq ((n + k) + 1) - newton_seq (n+k)∥) (∥newton_seq (n+k) - newton_seq n∥) : padic_norm_z.nonarchimedean _ _
id         └─┘  └────────┘             └────────┘       └────────┘      └────────┘     └─────────────────────────┘
src        └─┘  └────────┘              └────────┘        └────────┘       └────────┘      └─────────────────────────┘
typ        └─┘  └────────┘             └────────┘       └────────┘      └────────┘     └─────────────────────────┘
276  ... ≤ max (∥F.derivative.eval a∥ * T^(2^((n + k)))) (∥F.derivative.eval a∥ * T^(2^n)) :
id         └─┘  └─────────┘└───┘                └─────────┘└───┘     
src        └─┘   └─────────┘└───┘                   └─────────┘└───┘      
typ        └─┘  └─────────┘└───┘                └─────────┘└───┘     
doc               └─────────┘└───┘                         └─────────┘└───┘      
277    max_le_max (newton_seq_succ_dist _) (newton_seq_dist_aux _)
id     └────────┘  └──────────────────┘     └─────────────────┘
src    └────────┘  └──────────────────┘
typ    └────────┘  └──────────────────┘     └─────────────────┘
278  ... = ∥F.derivative.eval a∥ * T^(2^n) :
id         └─────────┘└───┘     
src         └─────────┘└───┘      
typ        └─────────┘└───┘     
doc          └─────────┘└───┘      
279    max_eq_right $ mul_le_mul_of_nonneg_left (pow_le_pow_of_le_one (norm_nonneg _) (le_of_lt T_lt_one) this) (norm_nonneg _)
id     └──────────┘   └───────────────────────┘  └──────────────────┘  └─────────┘     └──────┘ └──────┘  └──┘   └─────────┘
src    └──────────┘   └───────────────────────┘  └──────────────────┘  └─────────┘     └──────┘ └──────┘         └─────────┘
typ    └──────────┘   └───────────────────────┘  └──────────────────┘  └─────────┘     └──────┘ └──────┘  └──┘   └─────────┘
280  
281  private lemma newton_seq_dist {n k : ℕ} (hnk : n ≤ k) :
id                                                   
src                                                  
typ                                                  
282    ∥newton_seq k - newton_seq n∥ ≤ ∥F.derivative.eval a∥ * T^(2^n) :=
id     └────────┘   └────────┘   └─────────┘└───┘     
src    └────────┘    └────────┘     └─────────┘└───┘      
typ    └────────┘   └────────┘   └─────────┘└───┘     
doc                                      └─────────┘└───┘      
283  have hex : ∃ m, k = n + m, from exists_eq_add_of_le hnk,
id                           └─────────────────┘ └─┘
src                              └─────────────────┘
typ                          └─────────────────┘ └─┘
284  let ⟨_, hex'⟩ := hex in
id   └─┘              └─┘
typ  └─┘              └─┘
285  by rw hex'; apply newton_seq_dist_aux; assumption
id         └──┘        └─────────────────┘
src     └─┘      └────┘└─────────────────┘  └──────────
typ     └─┘└──┘  └────┘└─────────────────┘  └──────────
doc     └─┘      └────┘                     └──────────
txt     └─┘      └────┘                     └──────────
par     └─┘      └────┘                     └──────────
pid                                                 
st     └───────────────────────────────────────────────
286  
src  
typ  
doc  
txt  
par  
pid  
st   
287  private lemma newton_seq_dist_to_a : ∀ n : ℕ, 0 < n → ∥newton_seq n - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥
id                                                     └────────┘     └───┘   └─────────┘└───┘ 
src                                                      └────────┘        └───┘     └─────────┘└───┘  
typ                                                    └────────┘     └───┘   └─────────┘└───┘ 
doc                                                                               └───┘        └─────────┘└───┘
288  | 1 h := by simp [newton_seq, newton_seq_aux, ih_n]; apply norm_div
id                     └────────┘  └────────────┘  └──┘
src              └────┘└────────┘└┘└────────────┘└┘└──┘  └────┘        
typ              └────┘└────────┘└┘└────────────┘└┘└──┘  └────┘        
doc              └────┘          └┘              └┘└──┘  └────┘        
txt              └────┘          └┘              └┘      └────┘        
par              └────┘          └┘              └┘      └────┘        
pid                            └┘              └┘                   
st              └───────────────────────────────────────────────────────┘
289  | (k+2) h :=
id      
src      
typ     
290    have hlt : ∥newton_seq (k+2) - newton_seq (k+1)∥ < ∥newton_seq (k+1) - a∥,
id                └────────┘       └────────┘       └────────┘       
src               └────────┘       └────────┘       └────────┘        
typ               └────────┘       └────────┘       └────────┘       
291      by rw newton_seq_dist_to_a (k+1) (succ_pos _); apply newton_seq_succ_dist_weak; assumption,
id             └──────────────────┘      └──────┘           └───────────────────────┘
src         └─┘                      └─┘ └──────┘└─┘  └────┘└───────────────────────┘  └────────┘
typ         └─┘└──────────────────┘ └─┘ └──────┘└─┘  └────┘└───────────────────────┘  └────────┘
doc         └─┘                       └─┘         └─┘  └────┘                           └────────┘
txt         └─┘                       └─┘         └─┘  └────┘                           └────────┘
par         └─┘                       └─┘         └─┘  └────┘                           └────────┘
pid                                  └─┘         └─┘       
st         └──────────────────────────────────────────────────────────────────────────────────────┘
292    have hne' : ∥newton_seq (k + 2) - newton_seq (k+1)∥ ≠ ∥newton_seq (k+1) - a∥, from ne_of_lt hlt,
id                 └────────┘         └────────┘       └────────┘              └──────┘ └─┘
src                └────────┘         └────────┘       └────────┘               └──────┘
typ                └────────┘         └────────┘       └────────┘              └──────┘ └─┘
293    calc  ∥newton_seq (k + 2) - a∥
id           └────────┘         
src          └────────┘          
typ          └────────┘         
294      = ∥(newton_seq (k + 2) - newton_seq (k+1)) + (newton_seq (k+1) - a)∥ : by rw ←sub_add_sub_cancel
id          └────────┘         └────────┘         └────────┘                  └────────────────┘
src         └────────┘         └────────┘         └────────┘               └──┘└────────────────┘
typ         └────────┘         └────────┘         └────────┘              └──┘└────────────────┘
doc                                                                                └──┘                  
txt                                                                                └──┘                  
par                                                                                └──┘                  
pid                                                                                  └┘                  
st                                                                                └──────────────────────┘
295  ... = max (∥newton_seq (k + 2) - newton_seq (k+1)∥) (∥newton_seq (k+1) - a∥) : padic_norm_z.add_eq_max_of_ne hne'
id         └─┘  └────────┘         └────────┘        └────────┘           └───────────────────────────┘ └──┘
src        └─┘  └────────┘         └────────┘        └────────┘            └───────────────────────────┘
typ        └─┘  └────────┘         └────────┘        └────────┘           └───────────────────────────┘ └──┘
296  ... = ∥newton_seq (k+1) - a∥ : max_eq_right_of_lt hlt
id         └────────┘          └────────────────┘ └─┘
src        └────────┘           └────────────────┘
typ        └────────┘          └────────────────┘ └─┘
297  ... = ∥polynomial.eval a F∥ / ∥polynomial.eval a (polynomial.derivative F)∥ : newton_seq_dist_to_a (k+1) (succ_pos _)
id         └─────────────┘    └─────────────┘   └───────────────────┘     └──────────────────┘       └──────┘
src        └─────────────┘      └─────────────┘    └───────────────────┘                                 └──────┘
typ        └─────────────┘    └─────────────┘   └───────────────────┘     └──────────────────┘       └──────┘
doc         └─────────────┘         └─────────────┘    └───────────────────┘
298  
299  private lemma bound' : tendsto (λ n : ℕ, ∥F.derivative.eval a∥ * T^(2^n)) at_top (𝓝 0) :=
id                          └─────┘          └─────────┘└───┘        └────┘  
src                         └─────┘           └─────────┘└───┘          └────┘  
typ                         └─────┘          └─────────┘└───┘        └────┘  
doc                         └─────┘             └─────────┘└───┘              └────┘  
300  begin
st   └─────
301    rw ←mul_zero (∥F.derivative.eval a∥),
id         └──────┘  └───────────────┘ 
src    └──┘└──────┘ └───────────────┘ 
typ    └──┘└──────┘ └───────────────┘
doc    └──┘          └───────────────┘  
txt    └──┘                             
par    └──┘                             
pid      └┘                             
st   ─────────────────────────────────────┘└─
302    exact tendsto_const_nhds.mul
id           └────────────────────┘
src    └────┘└────────────────────┘
typ    └────┘└────────────────────┘
doc    └────┘                      
txt    └────┘                      
par    └────┘                      
pid                               
st   ───────────────────────────────
303                      (tendsto.comp
id                        └──────────┘
src  ───────────────────┘ └──────────┘
typ  ───────────────────┘ └──────────┘
doc  ───────────────────┘             
txt  ───────────────────┘             
par  ───────────────────┘             
pid  ───────────────────┘             
st   ──────────────────────────────────
304                        (tendsto_pow_at_top_nhds_0_of_lt_1 (norm_nonneg _) (T_lt_one hnorm))
id                          └───────────────────────────────┘  └─────────┘     └──────┘ └───┘
src  ─────────────────────┘ └───────────────────────────────┘ └─────────┘└──┘ └──────┘     └──
typ  ─────────────────────┘ └───────────────────────────────┘ └─────────┘└──┘ └──────┘└───┘└──
doc  ─────────────────────┘                                              └──┘              └──
txt  ─────────────────────┘                                              └──┘              └──
par  ─────────────────────┘                                              └──┘              └──
pid  ─────────────────────┘                                              └──┘              └──
st   ───────────────────────────────────────────────────────────────────────────────────────────
305                        (tendsto_pow_at_top_at_top_of_gt_1_nat (by norm_num)))
id                          └───────────────────────────────────┘
src  ─────────────────────┘ └───────────────────────────────────┘   └──────┘└──┘
typ  ─────────────────────┘ └───────────────────────────────────┘   └──────┘└──┘
doc  ─────────────────────┘                                         └──────┘└──┘
txt  ─────────────────────┘                                         └──────┘└──┘
par  ─────────────────────┘                                         └──────┘└──┘
pid  ─────────────────────┘                                         └──────────┘
st   ───────────────────────────────────────────────────────────────┘└───────┘└──┘
306  end
st   └─┘
307  
308  private lemma bound : ∀ {ε}, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → ∥F.derivative.eval a∥ * T^(2^n) < ε :=
id                                                      └─────────┘└───┘        
src                                                           └─────────┘└───┘         
typ                                                     └─────────┘└───┘        
doc                                                                 └─────────┘└───┘      
309  have mtn : ∀ n : ℕ, ∥polynomial.eval a (polynomial.derivative F)∥ * T ^ (2 ^ n) ≥ 0,
id                      └─────────────┘   └───────────────────┘            
src                     └─────────────┘    └───────────────────┘              
typ                     └─────────────┘   └───────────────────┘            
doc                       └─────────────┘    └───────────────────┘       
310    from λ n, mul_nonneg (norm_nonneg _) (T_pow_nonneg _),
id              └────────┘  └─────────┘     └──────────┘
src              └────────┘  └─────────┘     └──────────┘
typ             └────────┘  └─────────┘     └──────────┘
311  begin
st   └─────
312    have := bound' hnorm hnsol,
id             └────┘ └───┘ └───┘
src    └──────┘└────┘     
typ    └──────┘└────┘└───┘└───┘
doc    └──────┘           
txt    └──────┘           
par    └──────┘           
pid    └───┘└─┘           
st   ───────────────────────────┘└─
313    simp [tendsto, nhds] at this,
id           └─────┘  └──┘
src    └────┘└─────┘└┘└──┘└───────┘
typ    └────┘└─────┘└┘└──┘└───────┘
doc    └────┘└─────┘└┘└──┘└───────┘
txt    └────┘       └┘    └───────┘
par    └────┘       └┘    └───────┘
pid               └┘    └─────┘
st   ─────────────────────────────┘└─
314    intros ε hε,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
315    cases this (ball 0 ε) (mem_ball_self hε) (is_open_ball) with N hN,
id           └──┘  └──┘      └───────────┘ └┘   └──────────┘
src    └────┘     └──┘└─┘ └┘ └───────────┘  └┘ └──────────┘└─────────┘
typ    └────┘└──┘ └──┘└─┘└┘ └───────────┘└┘└┘ └──────────┘└─────────┘
doc    └────┘     └──┘└─┘ └┘                └┘             └─────────┘
txt    └────┘         └─┘ └┘                └┘             └─────────┘
par    └────┘         └─┘ └┘                └┘             └─────────┘
pid                  └─┘ └┘                └┘             └────────┘
st   ──────────────────────────────────────────────────────────────────┘└─
316    existsi N, intros n hn,
id             
src    └──────┘   └─────────┘
typ    └──────┘  └─────────┘
doc    └──────┘   └─────────┘
txt    └──────┘   └─────────┘
par    └──────┘   └─────────┘
pid                    └───┘
st   ──────────┘└───────────┘└─
317    simpa [normed_field.norm_mul, real.norm_eq_abs, abs_of_nonneg (mtn n)] using hN _ hn
id            └───────────────────┘  └──────────────┘  └───────────┘  └─┘          └┘   └┘
src    └─────┘└───────────────────┘└┘└──────────────┘└┘└───────────┘     └───────┘  └─┘  
typ    └─────┘└───────────────────┘└┘└──────────────┘└┘└───────────┘ └─┘└───────┘└┘└─┘└┘
doc    └─────┘                     └┘                └┘                  └───────┘  └─┘  
txt    └─────┘                     └┘                └┘                  └───────┘  └─┘  
par    └─────┘                     └┘                └┘                  └───────┘  └─┘  
pid                              └┘                └┘                  └┘└────┘  └─┘  
st   ──────────────────────────────────────────────────────────────────────────────────────┘
318  end
st   └─┘
319  
320  private lemma bound'_sq : tendsto (λ n : ℕ, ∥F.derivative.eval a∥^2 * T^(2^n)) at_top (𝓝 0) :=
id                             └─────┘          └─────────┘└───┘         └────┘  
src                            └─────┘           └─────────┘└───┘           └────┘  
typ                            └─────┘          └─────────┘└───┘         └────┘  
doc                            └─────┘             └─────────┘└───┘                └────┘  
321  begin
st   └─────
322    rw [←mul_zero (∥F.derivative.eval a∥), _root_.pow_two],
id          └──────┘  └───────────────┘    └────────────┘
src    └───┘└──────┘ └───────────────┘ └─┘└────────────┘
typ    └───┘└──────┘ └───────────────┘└─┘└────────────┘
doc    └───┘          └───────────────┘  └─┘              
txt    └───┘                             └─┘              
par    └───┘                             └─┘              
pid      └─┘                             └─┘              
st   ──────────────────────────────────────┘└──────────────┘└──
323    simp only [mul_assoc],
id                └───────┘
src    └─────────┘└───────┘
typ    └─────────┘└───────┘
doc    └─────────┘         
txt    └─────────┘         
par    └─────────┘         
pid        └──┘└┘         
st   ──────────────────────┘└─
324    apply tendsto.mul,
id           └─────────┘
src    └────┘└─────────┘
typ    └────┘└─────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────┘└─
325    { apply tendsto_const_nhds },
id             └────────────────┘
src      └────┘└────────────────┘
typ      └────┘└────────────────┘
doc      └────┘                  
txt      └────┘                  
par      └────┘                  
pid                             
st   ───┘└───────────────────────┘└┘
326    { apply bound', assumption }
id             └────┘
src      └────┘└────┘  └─────────┘
typ      └────┘└────┘  └─────────┘
doc      └────┘        └─────────┘
txt      └────┘        └─────────┘
par      └────┘        └─────────┘
pid                             
st   ───────────────┘└───────────┘└─
327  end
st   ──┘
328  
329  private theorem newton_seq_is_cauchy : is_cau_seq norm newton_seq :=
id                                          └────────┘ └──┘ └────────┘
src                                         └────────┘ └──┘ └────────┘
typ                                         └────────┘ └──┘ └────────┘
doc                                         └────────┘
330  begin
st   └─────
331    intros ε hε,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
332    cases bound hnorm hnsol hε with N hN,
id           └───┘ └───┘ └───┘ └┘
src    └────┘└───┘            └────────┘
typ    └────┘└───┘└───┘└───┘└┘└────────┘
doc    └────┘                 └────────┘
txt    └────┘                 └────────┘
par    └────┘                 └────────┘
pid                          └────────┘
st   ─────────────────────────────────────┘└─
333    existsi N,
id             
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ──────────┘└─
334    intros j hj,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid          └───┘
st   ────────────┘└─
335    apply lt_of_le_of_lt,
id           └────────────┘
src    └────┘└────────────┘
typ    └────┘└────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────┘└─
336    { apply newton_seq_dist _ _ hj, assumption },
id             └─────────────┘     └┘
src      └────┘└─────────────┘└───┘    └─────────┘
typ      └────┘└─────────────┘└───┘└┘  └─────────┘
doc      └────┘               └───┘    └─────────┘
txt      └────┘               └───┘    └─────────┘
par      └────┘               └───┘    └─────────┘
pid                          └───┘              
st   ───┘└──────────────────────────┘└───────────┘└┘
337    { apply hN, apply le_refl }
id                       └─────┘
src      └────┘    └────┘└─────┘
typ      └────┘    └────┘└─────┘
doc      └────┘    └────┘       
txt      └────┘    └────┘       
par      └────┘    └────┘       
pid                           
st   ───────────┘└──────────────┘└─
338  end
st   ──┘
339  
340  private def newton_cau_seq : cau_seq ℤ_[p] norm := ⟨_, newton_seq_is_cauchy⟩
id                                └─────┘ └─┘ └──┘        └──────────────────┘
src                               └─────┘ └─┘  └──┘        └──────────────────┘
typ                               └─────┘ └─┘ └──┘        └──────────────────┘
doc                                       └─┘ 
341  
342  private def soln : ℤ_[p] := newton_cau_seq.lim
id                      └─┘    └────────────┘└──┘
src                     └─┘     └────────────┘└──┘
typ                     └─┘    └────────────┘└──┘
doc                     └─┘ 
343  
344  private lemma soln_spec {ε : ℝ} (hε : ε > 0) :
id                                         
src                                         
typ                                        
345    ∃ (N : ℕ), ∀ {i : ℕ}, i ≥ N → ∥soln - newton_cau_seq i∥ < ε :=
id                            └──┘  └────────────┘   
src                             └──┘  └────────────┘   
typ                           └──┘  └────────────┘   
346  setoid.symm (cau_seq.equiv_lim newton_cau_seq) _ hε
id   └─────────┘  └───────────────┘ └────────────┘    └┘
src  └─────────┘  └───────────────┘ └────────────┘
typ  └─────────┘  └───────────────┘ └────────────┘    └┘
347  
348  private lemma soln_deriv_norm : ∥F.derivative.eval soln∥ = ∥F.derivative.eval a∥ :=
id                                   └─────────┘└───┘ └──┘  └─────────┘└───┘ 
src                                   └─────────┘└───┘ └──┘   └─────────┘└───┘  
typ                                  └─────────┘└───┘ └──┘  └─────────┘└───┘ 
doc                                    └─────────┘└───┘           └─────────┘└───┘
349  norm_deriv_eq newton_seq_deriv_norm
id   └───────────┘ └───────────────────┘
src  └───────────┘ └───────────────────┘
typ  └───────────┘ └───────────────────┘
350  
351  private lemma newton_seq_norm_tendsto_zero : tendsto (λ i, ∥F.eval (newton_cau_seq i)∥) at_top (𝓝 0) :=
id                                                └─────┘      └───┘  └────────────┘    └────┘  
src                                               └─────┘        └───┘  └────────────┘     └────┘  
typ                                               └─────┘      └───┘  └────────────┘    └────┘  
doc                                               └─────┘         └───┘                      └────┘  
352  squeeze_zero (λ _, norm_nonneg _) newton_seq_norm_le bound'_sq
id   └──────────┘      └─────────┘    └────────────────┘ └───────┘
src  └──────────┘       └─────────┘    └────────────────┘ └───────┘
typ  └──────────┘      └─────────┘    └────────────────┘ └───────┘
353  
354  private lemma newton_seq_dist_tendsto :
355    tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (𝓝 (∥F.eval a∥ / ∥F.derivative.eval a∥)) :=
id     └─────┘      └────────────┘     └────┘    └───┘   └─────────┘└───┘ 
src    └─────┘       └────────────┘       └────┘     └───┘     └─────────┘└───┘  
typ    └─────┘      └────────────┘     └────┘    └───┘   └─────────┘└───┘ 
doc    └─────┘                               └────┘      └───┘        └─────────┘└───┘
356  tendsto.congr'
id   └────────────┘
src  └────────────┘
typ  └────────────┘
357    (suffices ∃ k, ∀ n ≥ k,  ∥F.eval a∥ / ∥F.derivative.eval a∥ = ∥newton_cau_seq n - a∥, by simpa,
id                         └───┘   └─────────┘└───┘   └────────────┘   
src                           └───┘     └─────────┘└───┘    └────────────┘          └───┘
typ                        └───┘   └─────────┘└───┘   └────────────┘        └───┘
doc                               └───┘        └─────────┘└───┘                                 └───┘
txt                                                                                             └───┘
par                                                                                             └───┘
st                                                                                             └────┘
358      ⟨1, λ _ hx, (newton_seq_dist_to_a _ hx).symm⟩)
id              └┘   └──────────────────┘   └┘ └──┘
src                   └──────────────────┘      └──┘
typ             └┘   └──────────────────┘   └┘ └──┘
359    (tendsto_const_nhds)
id      └────────────────┘
src     └────────────────┘
typ     └────────────────┘
360  
361  private lemma newton_seq_dist_tendsto' :
362    tendsto (λ n, ∥newton_cau_seq n - a∥) at_top (𝓝 ∥soln - a∥) :=
id     └─────┘      └────────────┘     └────┘   └──┘  
src    └─────┘       └────────────┘       └────┘   └──┘   
typ    └─────┘      └────────────┘     └────┘   └──┘  
doc    └─────┘                               └────┘  
363  (continuous_norm.tendsto _).comp (newton_cau_seq.tendsto_limit.sub tendsto_const_nhds)
id    └─────────────┘└──────┘   └──┘   └────────────┘└────────────┘└──┘ └────────────────┘
src   └─────────────┘└──────┘   └──┘   └────────────┘└────────────┘└──┘ └────────────────┘
typ   └─────────────┘└──────┘   └──┘   └────────────┘└────────────┘└──┘ └────────────────┘
364  
365  private lemma soln_dist_to_a : ∥soln - a∥ = ∥F.eval a∥ / ∥F.derivative.eval a∥ :=
id                                  └──┘    └───┘   └─────────┘└───┘ 
src                                 └──┘      └───┘     └─────────┘└───┘  
typ                                 └──┘    └───┘   └─────────┘└───┘ 
doc                                                └───┘        └─────────┘└───┘
366  tendsto_nhds_unique at_top_ne_bot newton_seq_dist_tendsto' newton_seq_dist_tendsto
id   └─────────────────┘ └───────────┘ └──────────────────────┘ └─────────────────────┘
src  └─────────────────┘ └───────────┘ └──────────────────────┘ └─────────────────────┘
typ  └─────────────────┘ └───────────┘ └──────────────────────┘ └─────────────────────┘
367  
368  private lemma soln_dist_to_a_lt_deriv : ∥soln - a∥ < ∥F.derivative.eval a∥ :=
id                                           └──┘    └─────────┘└───┘ 
src                                          └──┘      └─────────┘└───┘  
typ                                          └──┘    └─────────┘└───┘ 
doc                                                         └─────────┘└───┘
369  begin
st   └─────
370    rw soln_dist_to_a,
id        └────────────┘
src    └─┘└────────────┘
typ    └─┘└────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────┘└─
371    apply div_lt_of_mul_lt_of_pos,
id           └─────────────────────┘
src    └────┘└─────────────────────┘
typ    └────┘└─────────────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ──────────────────────────────┘└─
372    { apply deriv_norm_pos; assumption },
id             └────────────┘
src      └────┘└────────────┘  └─────────┘
typ      └────┘└────────────┘  └─────────┘
doc      └────┘                └─────────┘
txt      └────┘                └─────────┘
par      └────┘                └─────────┘
pid                                     
st   ───┘└───────────────────────────────┘└┘
373    { rwa _root_.pow_two at hnorm }
id           └────────────┘
src      └──┘└────────────┘└────────┘
typ      └──┘└────────────┘└────────┘
doc      └──┘              └────────┘
txt      └──┘              └────────┘
par      └──┘              └────────┘
pid                       └───────┘
st   ───────────────────────────────┘└─
374  end
st   ──┘
375  
376  private lemma eval_soln : F.eval soln = 0 :=
id                             └───┘ └──┘ 
src                             └───┘ └──┘ 
typ                            └───┘ └──┘ 
doc                             └───┘
377  limit_zero_of_norm_tendsto_zero newton_seq_norm_tendsto_zero
id   └─────────────────────────────┘ └──────────────────────────┘
src  └─────────────────────────────┘ └──────────────────────────┘
typ  └─────────────────────────────┘ └──────────────────────────┘
378  
379  private lemma soln_unique (z : ℤ_[p]) (hev : F.eval z = 0) (hnlt : ∥z - a∥ < ∥F.derivative.eval a∥) :
id                                  └─┘         └───┘                  └─────────┘└───┘ 
src                                 └─┘           └───┘                      └─────────┘└───┘  
typ                                 └─┘         └───┘                  └─────────┘└───┘ 
doc                                 └─┘           └───┘                            └─────────┘└───┘
380    z = soln :=
id       └──┘
src       └──┘
typ      └──┘
381  have soln_dist : ∥z - soln∥ < ∥F.derivative.eval a∥, from calc
id                      └──┘  └─────────┘└───┘ 
src                      └──┘   └─────────┘└───┘  
typ                     └──┘  └─────────┘└───┘ 
doc                                  └─────────┘└───┘
382    ∥z - soln∥ = ∥(z - a) + (a - soln)∥ : by rw sub_add_sub_cancel
id       └──┘            └──┘          └────────────────┘
src       └──┘               └──┘       └─┘└────────────────┘
typ      └──┘            └──┘       └─┘└────────────────┘
doc                                             └─┘                  
txt                                             └─┘                  
par                                             └─┘                  
pid                                                                 
st                                             └──────────────────────
383          ... ≤ max (∥z - a∥) (∥a - soln∥) : padic_norm_z.nonarchimedean _ _
id                 └─┘         └──┘    └─────────────────────────┘
src  ───────┘      └─┘            └──┘    └─────────────────────────┘
typ  ───────┘      └─┘         └──┘    └─────────────────────────┘
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘
384          ... < ∥F.derivative.eval a∥ : max_lt hnlt (by rw norm_sub_rev; apply soln_dist_to_a_lt_deriv),
id                 └─────────┘└───┘    └────┘ └──┘        └──────────┘        └─────────────────────┘
src                 └─────────┘└───┘     └────┘          └─┘└──────────┘  └────┘└─────────────────────┘
typ                └─────────┘└───┘    └────┘ └──┘     └─┘└──────────┘  └────┘└─────────────────────┘
doc                  └─────────┘└───┘                      └─┘              └────┘
txt                                                        └─┘              └────┘
par                                                        └─┘              └────┘
pid                                                                             
st                                                        └─────────────────────────────────────────────┘
385  let h := z - soln,
id   └─┘       └──┘
src              └──┘
typ  └─┘       └──┘
386      ⟨q, hq⟩ := F.binom_expansion soln h in
id                 └──────────────┘ └──┘ 
src                  └──────────────┘ └──┘
typ                └──────────────┘ └──┘ 
387  have (F.derivative.eval soln + q * h) * h = 0, from eq.symm (calc
id         └─────────┘└───┘ └──┘                  └─────┘
src         └─────────┘└───┘ └──┘                    └─────┘
typ        └─────────┘└───┘ └──┘                  └─────┘
doc         └─────────┘└───┘
388    0 = F.eval (soln + h) : by simp [hev, h]
id         └───┘  └──┘               └─┘  
src         └───┘  └──┘          └────┘   └┘ └┘
typ        └───┘  └──┘         └────┘└─┘└┘└┘
doc         └───┘                 └────┘   └┘ └┘
txt                               └────┘   └┘ └┘
par                               └────┘   └┘ └┘
pid                                      └┘ 
st                               └─────────────┘
389  ... = F.derivative.eval soln * h + q * h^2 : by rw [hq, eval_soln, zero_add]
id         └─────────┘└───┘ └──┘                  └┘  └───────┘  └──────┘
src         └─────────┘└───┘ └──┘                └──┘  └┘└───────┘└┘└──────┘└┘
typ        └─────────┘└───┘ └──┘              └──┘└┘└┘└───────┘└┘└──────┘└┘
doc         └─────────┘└───┘                         └──┘  └┘         └┘        └┘
txt                                                  └──┘  └┘         └┘        └┘
par                                                  └──┘  └┘         └┘        └┘
pid                                                    └┘  └┘         └┘        
st                                                  └─────┘└─────────┘└────────┘
390  ... = (F.derivative.eval soln + q * h) * h : by rw [_root_.pow_two, right_distrib, mul_assoc]),
id          └─────────┘└───┘ └──┘                  └────────────┘  └───────────┘  └───────┘
src          └─────────┘└───┘ └──┘                └──┘└────────────┘└┘└───────────┘└┘└───────┘
typ         └─────────┘└───┘ └──┘              └──┘└────────────┘└┘└───────────┘└┘└───────┘
doc          └─────────┘└───┘                        └──┘              └┘             └┘         
txt                                                  └──┘              └┘             └┘         
par                                                  └──┘              └┘             └┘         
pid                                                    └┘              └┘             └┘         
st                                                  └─────────────────┘└─────────────┘└─────────┘
391  have h = 0, from by_contradiction $ λ hne,
id                  └──────────────┘     └─┘
src                  └──────────────┘
typ                 └──────────────┘     └─┘
392    have F.derivative.eval soln + q * h = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
id          └─────────┘└───┘ └──┘                └───────────────────────────────┘ └──┘ └───────────┘  └─┘
src          └─────────┘└───┘ └──┘                 └───────────────────────────────┘      └───────────┘
typ         └─────────┘└───┘ └──┘                └───────────────────────────────┘ └──┘ └───────────┘  └─┘
doc          └─────────┘└───┘
393    have F.derivative.eval soln = (-q) * h, by simpa using eq_neg_of_add_eq_zero this,
id          └─────────┘└───┘ └──┘                        └───────────────────┘ └──┘
src          └─────────┘└───┘ └──┘             └──────────┘└───────────────────┘
typ         └─────────┘└───┘ └──┘            └──────────┘└───────────────────┘└──┘
doc          └─────────┘└───┘                     └──────────┘                     
txt                                               └──────────┘                     
par                                               └──────────┘                     
pid                                                    └────┘                     
st                                               └─────────────────────────────────────┘
394    lt_irrefl ∥F.derivative.eval soln∥ (calc
id     └───────┘ └─────────┘└───┘ └──┘
src    └───────┘  └─────────┘└───┘ └──┘
typ    └───────┘ └─────────┘└───┘ └──┘
doc                └─────────┘└───┘
395    ∥F.derivative.eval soln∥ = ∥(-q) * h∥ : by rw this
id     └─────────┘└───┘ └──┘                 └──┘
src     └─────────┘└───┘ └──┘               └─┘    
typ    └─────────┘└───┘ └──┘              └─┘└──┘
doc      └─────────┘└───┘                         └─┘    
txt                                               └─┘    
par                                               └─┘    
pid                                                     
st                                               └───────┘
396  ... ≤ 1 * ∥h∥ : by rw [padic_norm_z.mul]; exact mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (norm_nonneg _)
id                      └──────────────┘         └────────────────────────┘  └─────────────────┘     └─────────┘
src                  └──┘└──────────────┘  └────┘└────────────────────────┘ └─────────────────┘└──┘ └─────────┘└──┘
typ                 └──┘└──────────────┘  └────┘└────────────────────────┘ └─────────────────┘└──┘ └─────────┘└──┘
doc                     └──┘                  └────┘                                              └──┘            └──┘
txt                     └──┘                  └────┘                                              └──┘            └──┘
par                     └──┘                  └────┘                                              └──┘            └──┘
pid                       └┘                                                                     └──┘            └─┘
st                     └───────────────────┘└─────────────────────────────────────────────────────────────────────────┘
397  ... = ∥z - soln∥ : by simp [h]
id           └──┘            
src           └──┘      └────┘ └┘
typ          └──┘      └────┘└┘
doc                        └────┘ └┘
txt                        └────┘ └┘
par                        └────┘ └┘
pid                             
st                        └────────┘
398  ... < ∥F.derivative.eval soln∥ : by rw soln_deriv_norm; apply soln_dist),
id         └─────────┘└───┘ └──┘         └─────────────┘
src         └─────────┘└───┘ └──┘      └─┘└─────────────┘  └────┘
typ        └─────────┘└───┘ └──┘      └─┘└─────────────┘  └────┘
doc          └─────────┘└───┘            └─┘                 └────┘
txt                                      └─┘                 └────┘
par                                      └─┘                 └────┘
pid                                                              
st                                      └──────────────────────────────────┘
399  eq_of_sub_eq_zero (by rw ←this; refl)
id   └───────────────┘         └──┘
src  └───────────────┘     └──┘      └──┘
typ  └───────────────┘     └──┘└──┘  └──┘
doc                        └──┘      └──┘
txt                        └──┘      └──┘
par                        └──┘      └──┘
pid                          └┘
st                        └─────────────┘
400  
401  end hensel
402  
403  variables {p : ℕ} [nat.prime p] {F : polynomial ℤ_[p]} {a : ℤ_[p]}
id                     └───────┘         └────────┘ └─┘        └─┘ 
src                    └───────┘         └────────┘ └─┘        └─┘ 
typ                    └───────┘         └────────┘ └─┘        └─┘ 
doc                     └───────┘         └────────┘ └─┘        └─┘ 
404  
405  private lemma a_soln_is_unique (ha : F.eval a = 0) (z' : ℤ_[p]) (hz' : F.eval z' = 0)
id                                        └───┘            └─┘         └───┘ └┘ 
src                                        └───┘             └─┘           └───┘    
typ                                       └───┘            └─┘         └───┘ └┘ 
doc                                        └───┘              └─┘           └───┘
406    (hnormz' : ∥z' - a∥ < ∥F.derivative.eval a∥) : z' = a :=
id                └┘    └─────────┘└───┘     └┘  
src                       └─────────┘└───┘         
typ               └┘    └─────────┘└───┘     └┘  
doc                            └─────────┘└───┘
407  let h := z' - a,
id   └─┘     └┘  
src              
typ  └─┘     └┘  
408      ⟨q, hq⟩ := F.binom_expansion a h in
id                 └──────────────┘  
src                  └──────────────┘
typ                └──────────────┘  
409  have (F.derivative.eval a + q * h) * h = 0, from eq.symm (calc
id         └─────────┘└───┘                   └─────┘
src         └─────────┘└───┘                      └─────┘
typ        └─────────┘└───┘                   └─────┘
doc         └─────────┘└───┘
410    0 = F.eval (a + h) : show 0 = F.eval (a + (z' - a)), by rw add_comm; simp [hz']
id         └───┘                └───┘     └┘            └──────┘        └─┘
src         └───┘                   └───┘                  └─┘└──────┘  └────┘   └┘
typ        └───┘                └───┘     └┘         └─┘└──────┘  └────┘└─┘└┘
doc         └───┘                     └───┘                    └─┘          └────┘   └┘
txt                                                            └─┘          └────┘   └┘
par                                                            └─┘          └────┘   └┘
pid                                                                               
st                                                            └───────────────────────┘
411  ... = F.derivative.eval a * h + q * h^2 : by rw [hq, ha, zero_add]
id         └─────────┘└───┘                   └┘  └┘  └──────┘
src         └─────────┘└───┘                  └──┘  └┘  └┘└──────┘└┘
typ        └─────────┘└───┘               └──┘└┘└┘└┘└┘└──────┘└┘
doc         └─────────┘└───┘                      └──┘  └┘  └┘        └┘
txt                                               └──┘  └┘  └┘        └┘
par                                               └──┘  └┘  └┘        └┘
pid                                                 └┘  └┘  └┘        
st                                               └─────┘└──┘└────────┘
412  ... = (F.derivative.eval a + q * h) * h : by rw [_root_.pow_two, right_distrib, mul_assoc]),
id          └─────────┘└───┘                   └────────────┘  └───────────┘  └───────┘
src          └─────────┘└───┘                  └──┘└────────────┘└┘└───────────┘└┘└───────┘
typ         └─────────┘└───┘               └──┘└────────────┘└┘└───────────┘└┘└───────┘
doc          └─────────┘└───┘                     └──┘              └┘             └┘         
txt                                               └──┘              └┘             └┘         
par                                               └──┘              └┘             └┘         
pid                                                 └┘              └┘             └┘         
st                                               └─────────────────┘└─────────────┘└─────────┘
413  have h = 0, from by_contradiction $ λ hne,
id                  └──────────────┘     └─┘
src                  └──────────────┘
typ                 └──────────────┘     └─┘
414    have F.derivative.eval a + q * h = 0, from (eq_zero_or_eq_zero_of_mul_eq_zero this).resolve_right hne,
id          └─────────┘└───┘                 └───────────────────────────────┘ └──┘ └───────────┘  └─┘
src          └─────────┘└───┘                   └───────────────────────────────┘      └───────────┘
typ         └─────────┘└───┘                 └───────────────────────────────┘ └──┘ └───────────┘  └─┘
doc          └─────────┘└───┘
415    have F.derivative.eval a = (-q) * h, by simpa using eq_neg_of_add_eq_zero this,
id          └─────────┘└───┘                         └───────────────────┘ └──┘
src          └─────────┘└───┘               └──────────┘└───────────────────┘
typ         └─────────┘└───┘             └──────────┘└───────────────────┘└──┘
doc          └─────────┘└───┘                  └──────────┘                     
txt                                            └──────────┘                     
par                                            └──────────┘                     
pid                                                 └────┘                     
st                                            └─────────────────────────────────────┘
416    lt_irrefl ∥F.derivative.eval a∥ (calc
id     └───────┘ └─────────┘└───┘ 
src    └───────┘  └─────────┘└───┘  
typ    └───────┘ └─────────┘└───┘ 
doc                └─────────┘└───┘
417      ∥F.derivative.eval a∥ = ∥q∥*∥h∥ : by simp [this]
id       └─────────┘└───┘                 └──┘
src       └─────────┘└───┘             └────┘    └─
typ      └─────────┘└───┘           └────┘└──┘└─
doc        └─────────┘└───┘                   └────┘    └─
txt                                           └────┘    └─
par                                           └────┘    └─
pid                                                   
st                                           └────────────
418      ... ≤ 1*∥h∥ : mul_le_mul_of_nonneg_right (padic_norm_z.le_one _) (norm_nonneg _)
id                 └────────────────────────┘  └─────────────────┘     └─────────┘
src  ───┘           └────────────────────────┘  └─────────────────┘     └─────────┘
typ  ───┘          └────────────────────────┘  └─────────────────┘     └─────────┘
doc  ───┘
txt  ───┘
par  ───┘
pid  ───┘
st   ───┘
419      ... < ∥F.derivative.eval a∥ : by simpa [h]),
id             └─────────┘└───┘              
src             └─────────┘└───┘        └─────┘ 
typ            └─────────┘└───┘       └─────┘
doc              └─────────┘└───┘         └─────┘ 
txt                                       └─────┘ 
par                                       └─────┘ 
pid                                             
st                                       └────────┘
420  eq_of_sub_eq_zero (by rw ←this; refl)
id   └───────────────┘         └──┘
src  └───────────────┘     └──┘      └──┘
typ  └───────────────┘     └──┘└──┘  └──┘
doc                        └──┘      └──┘
txt                        └──┘      └──┘
par                        └──┘      └──┘
pid                          └┘
st                        └─────────────┘
421  
422  variable (hnorm : ∥F.eval a∥ < ∥F.derivative.eval a∥^2)
id                      └───┘     └─────────┘└───┘  
src                     └───┘     └─────────┘└───┘  
typ                     └───┘     └─────────┘└───┘  
doc                      └───┘        └─────────┘└───┘
423  include hnorm
424  
425  private lemma a_is_soln (ha : F.eval a = 0) :
id                                 └───┘  
src                                 └───┘   
typ                                └───┘  
doc                                 └───┘
426    F.eval a = 0 ∧ ∥a - a∥ < ∥F.derivative.eval a∥ ∧ ∥F.derivative.eval a∥ = ∥F.derivative.eval a∥ ∧
id     └───┘          └─────────┘└───┘   └─────────┘└───┘   └─────────┘└───┘  
src     └───┘              └─────────┘└───┘     └─────────┘└───┘     └─────────┘└───┘   
typ    └───┘          └─────────┘└───┘   └─────────┘└───┘   └─────────┘└───┘  
doc     └───┘                     └─────────┘└───┘        └─────────┘└───┘        └─────────┘└───┘
427    ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = a :=
id       └┘  └───┘ └┘      └┘    └─────────┘└───┘    └┘  
src           └───┘                 └─────────┘└───┘        
typ      └┘  └───┘ └┘      └┘    └─────────┘└───┘    └┘  
doc           └───┘                       └─────────┘└───┘
428  ⟨ha, by simp; apply deriv_norm_pos; apply hnorm, rfl, a_soln_is_unique ha⟩
id    └┘                 └────────────┘               └─┘  └──────────────┘ └┘
src          └──┘  └────┘└────────────┘  └────┘       └─┘  └──────────────┘
typ   └┘     └──┘  └────┘└────────────┘  └────┘       └─┘  └──────────────┘ └┘
doc          └──┘  └────┘                └────┘
txt          └──┘  └────┘                └────┘
par          └──┘  └────┘                └────┘
pid                                          
st          └──────────────────────────────────────┘
429  
430  lemma hensels_lemma : ∃ z : ℤ_[p], F.eval z = 0 ∧ ∥z - a∥ < ∥F.derivative.eval a∥ ∧
id                              └─┘ └───┘          └─────────┘└───┘  
src                             └─┘   └───┘              └─────────┘└───┘   
typ                             └─┘ └───┘          └─────────┘└───┘  
doc                              └─┘    └───┘                     └─────────┘└───┘
431    ∥F.derivative.eval z∥ = ∥F.derivative.eval a∥ ∧
id     └─────────┘└───┘   └─────────┘└───┘  
src     └─────────┘└───┘     └─────────┘└───┘   
typ    └─────────┘└───┘   └─────────┘└───┘  
doc      └─────────┘└───┘        └─────────┘└───┘
432    ∀ z', F.eval z' = 0 → ∥z' - a∥ < ∥F.derivative.eval a∥ → z' = z :=
id       └┘  └───┘ └┘      └┘    └─────────┘└───┘    └┘  
src           └───┘                 └─────────┘└───┘        
typ      └┘  └───┘ └┘      └┘    └─────────┘└───┘    └┘  
doc           └───┘                       └─────────┘└───┘
433  if ha : F.eval a = 0 then ⟨a, a_is_soln hnorm ha⟩ else
id   └┘      └───┘             └───────┘ └───┘ └┘
src  └┘       └───┘               └───────┘
typ  └┘      └───┘             └───────┘ └───┘ └┘
doc           └───┘
434  by refine ⟨soln _ _, eval_soln _ _, soln_dist_to_a_lt_deriv _ _, soln_deriv_norm _ _, soln_unique _ _⟩;
id              └──┘      └───────┘      └─────────────────────┘      └─────────────┘      └─────────┘
src     └─────┘ └──┘└────┘└───────┘└────┘└─────────────────────┘└────┘└─────────────┘└────┘└─────────┘└───┘
typ     └─────┘ └──┘└────┘└───────┘└────┘└─────────────────────┘└────┘└─────────────┘└────┘└─────────┘└───┘
doc     └─────┘     └────┘         └────┘                       └────┘               └────┘           └───┘
txt     └─────┘     └────┘         └────┘                       └────┘               └────┘           └───┘
par     └─────┘     └────┘         └────┘                       └────┘               └────┘           └───┘
pid                └────┘         └────┘                       └────┘               └────┘           └───┘
st     └─────────────────────────────────────────────────────────────────────────────────────────────────────
435     assumption
src     └────────┘
typ     └────────┘
doc     └────────┘
txt     └────────┘
par     └────────┘
st   ────────────┘